package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = Type.t
type t = subst
val find_exn : t -> var Scoped.t -> term Scoped.t
val get_var : t -> var Scoped.t -> term Scoped.t option
val deref : t -> term Scoped.t -> term Scoped.t
val apply : ?shift_vars:int -> Renaming.t -> t -> term Scoped.t -> term

Apply the substitution to the given term/type.

  • parameter renaming

    used to desambiguate free variables from distinct scopes

val bind : t -> var Scoped.t -> term Scoped.t -> t

Add v -> t to the substitution. Both terms have a context.

val update : t -> var Scoped.t -> term Scoped.t -> t

Replace v -> ? by v -> t in the substitution. Both terms have a context.

val of_list : ?init:t -> (var Scoped.t * term Scoped.t) list -> t