This modules implements extended substitution of DB variables in a term. This is typically used to: 1) infer a "most general" typing substitution from constraints gathered while inferring the type of the LHS of a rule. 2) apply the substitution to the RHS of the rule before typechecking it.
val identity : t
val is_identity : t -> bool
add sigma n t returns the substitution
sigma with the extra mapping
apply sigma n t applies the subsitution
t considered under
n lambda abstractions.
Same as apply, but outputting a boolean
true if the term is modified by the substitution.
Special substitution function corresponding to given ExSubst.t instance
sigma "in a smaller context": Assume
sigma a substitution in a context Gamma = Gamma' ; Delta with |Delta|=
i. Then this function represents the substitution
sigma in the context Gamma'. All variables of Delta are ignored and substitutes of the variables of Gamma' are unshifted. This may therefore raise UnshiftExn in case substitutes of variables of Gamma' refers to variables of Delta.
mk_idempotent sigma successively applies sigma to its mapped terms until this operation has no effect anymore.