Module Subst.FO

include SPECIALIZED with type term = Term.t
type term = Term.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.

raises InconsistentBinding

if v is already bound in the same context, to another term.

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

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

raises InconsistentBinding

if v is not yet bound in the same context.

val of_list : ?⁠init:t -> (var Scoped.t * term Scoped.t) list -> t
val bind' : t -> Type.t HVar.t Scoped.t -> term Scoped.t -> t
val apply_l : ?⁠shift_vars:int -> Renaming.t -> t -> term list Scoped.t -> term list
val of_list' : ?⁠init:t -> (Type.t HVar.t Scoped.t * term Scoped.t) list -> t
val map : (term -> term) -> t -> t
val iter : (Type.t HVar.t Scoped.t -> term Scoped.t -> unit) -> t -> unit
val filter : (Type.t HVar.t Scoped.t -> term Scoped.t -> bool) -> t -> t
val compose : scope:int -> t -> t -> t

Takes a substitution that might map a variable x to a term that containts loosely bound variables. It fixes the substitution so that all such variables are remaped to a fresh skolem

val unleak_variables : t -> t * Term.t list

Takes a substitution that might map a variable x to a term that containts loosely bound variables. It fixes the substitution so that all such variables are remaped to a fresh skolem

val subset_is_renaming : subset:term Scoped.t list -> res_scope:int -> t -> bool
val canonize_neg_vars : var_set:Logtk.InnerTerm.VarSet.t -> t
val canonize_all_vars : term -> term