Module type VarManager.SubstSig

module type SubstSig = sig .. end

type t 
Abstract type of substitutions
type var 
Abstract type of variables substituted
type var_container 
abstract type of containers of variables
val empty : t
The empty substitution, which has no effect when applied.
val singleton : var -> var -> t
Constructor for a substitution mapping one variable to a term.
val of_list : (var * var) list ->
t
Make a substitution from a list of bindings
val avoid : var_container ->
var_container -> t
avoid vars subvars returns a substitution that takes all variables in subvars to variables fresh in vars U subvars, respecting existential quantification / free variables.
val pp : Format.formatter -> t -> unit
Pretty printer.
val to_string : t -> string
Convert a substitution to a string
val apply : t -> var -> var
Apply a substitution to a variable
val partition : t -> t * t
partition theta will partition theta into (theta_1, theta_2) such that theta_1 contains all and only the mappings in theta from a free variable to either an anonymous variable or another free variable; that is theta_1 is the part of theta which is a proper (proof-theoretic) substitution.
val strip : t -> t
Removes all identity bindings from the substitution map
val mk_free_subst : var_container ->
var_container -> t
mk_free_subst avoid vs produces a substitution of pairwise distinct free variables (fresh for all the variables in avoid) for the variables in vs.
val mk_ex_subst : var_container ->
var_container -> t
mk_ex_subst avoid vs produces a substitution of pairwise distinct existentially quantified variables (fresh for all the variables in avoid) for the variables in vs.