module type SubstSig = sig .. end
type
Abstract type of substitutions
type
Abstract type of variables substituted
type
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.