Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Substitutions using DeBruijn indices.
type substitution = Basic.loc -> Basic.ident -> int -> int -> Term.termA substitution is a function mapping a variable (location, identifier and DB index) under a given number of lambda abstractions to a term. A substitution raises Not_found meaning that the variable is not subsituted.
val apply_subst : substitution -> int -> Term.term -> Term.termapply_subst subst n t applies subst to t under n lambda abstractions.
- Variables with DB index
k<nare considered "locally bound" and are never substituted. - Variables with DB index
k>=nmay be substituted ifk-nis mapped insigma.
unshift i t shifts every De Bruijn indices in t by -i. Raises UnshiftExn when t contains De Bruijn variables of indices k <i.
val psubst_l : Term.term Stdlib.Lazy.t Basic.LList.t -> Term.term -> Term.termpsubst_l l k t substitutes the first n De Bruijn variables (with n = length l) in t with the corresponding term in l. Unshifts n times the free variables with greater indices.
subst t u substitutes the first free De Bruijn variable with u in t. Unshifts the other free variables.
val subst_n : int -> Basic.ident -> Term.term -> Term.termsubst_n n y t substitutes the n-th free De Bruijn variable in t with a fresh variable named y becoming the first free variable in t. All others free variables are shifted by one preventing index collision.
val occurs : int -> Term.term -> booloccurs n t returns true if t contains the variable n.