Varsval closedn : int -> Constr.constr -> boolclosedn n M is true iff M is a (de Bruijn) closed term under n binders
val closed0 : Constr.constr -> boolclosed0 M is true iff M is a (de Bruijn) closed term
val noccurn : int -> Constr.constr -> boolnoccurn n M returns true iff Rel n does NOT occur in term M
val noccur_between : int -> int -> Constr.constr -> boolnoccur_between n m M returns true iff Rel p does NOT occur in term M for n <= p < n+m
val noccur_with_meta : int -> int -> Constr.constr -> boolChecking function for terms containing existential- or meta-variables. The function noccur_with_meta does not consider meta-variables applied to some terms (intended to be its local context) (for existential variables, it is necessarily the case)
val exliftn : Esubst.lift -> Constr.constr -> Constr.constrexliftn el c lifts c with arbitrary complex lifting el
val liftn : int -> int -> Constr.constr -> Constr.constrliftn n k c lifts by n indices greater than or equal to k in c Note that with respect to substitution calculi's terminology, n is the _shift_ and k is the _lift_.
val lift : int -> Constr.constr -> Constr.constrlift n c lifts by n the positive indexes in c
val liftn_rel_context : int -> int -> Constr.rel_context -> Constr.rel_contextSame as liftn for a context
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_contextSame as lift for a context
The type substl is the type of substitutions u₁..un of type some well-typed context Δ and defined in some environment Γ. Typing of substitutions is defined by:
Note that u₁..un is represented as a list with un at the head of the list, i.e. as [un;...;u₁].
A substl differs from an instance in that it includes the terms bound by lets while the latter does not. Also, their internal representations are in opposite order.
type substl = Constr.constr listThe type instance is the type of instances u₁..un of a well-typed context Δ (relatively to some environment Γ). Typing of instances is defined by:
ϕ(Δ,u₁..u{_n}) is the substitution obtained by adding lets of Δ to the instance so as to get a substitution (see subst_of_rel_context_instance below).Note that u₁..un is represented as an array with u1 at the head of the array, i.e. as [u₁;...;un]. In particular, it can directly be used with mkApp to build an applicative term f u₁..un whenever f is of some type forall Δ, T.
An instance differs from a substl in that it does not include the terms bound by lets while the latter does. Also, their internal representations are in opposite order.
An instance_list is the same as an instance but using a list instead of an array.
type instance = Constr.constr arraytype instance_list = Constr.constr listval subst_of_rel_context_instance : Constr.rel_context -> instance -> substlLet Γ be a context interleaving declarations x₁:T₁..xn:Tn and definitions y₁:=c₁..yp:=cp in some context Γ₀. Let u₁..un be an instance of Γ, i.e. an instance in Γ₀ of the xi. Then, subst_of_rel_context_instance_list Γ u₁..un returns the corresponding substitution of Γ, i.e. the appropriate interleaving σ of the u₁..un with the c₁..cp, all of them in Γ₀, so that a derivation Γ₀, Γ, Γ₁|- t:T can be instantiated into a derivation Γ₀, Γ₁ |- t[σ]:T[σ] using substnl σ |Γ₁| t. Note that the instance u₁..un is represented starting with u₁, as if usable in applist while the substitution is represented the other way round, i.e. ending with either u₁ or c₁, as if usable for substl.
val subst_of_rel_context_instance_list :
Constr.rel_context ->
instance_list ->
substlval adjust_rel_to_rel_context : ( 'a, 'b ) Context.Rel.pt -> int -> intTake an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in x:A;y:=b;z:C is 3, i.e. a reference to z)
val substnl : substl -> int -> Constr.constr -> Constr.constrsubstnl [a₁;...;an] k c substitutes in parallel a₁,...,an for respectively Rel(k+1),...,Rel(k+n) in c; it relocates accordingly indexes in an,...,a1 and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then Γ, Γ' ⊢ substnl [a₁;...;an] k c : substnl [a₁;...;an] k T.
val substl : substl -> Constr.constr -> Constr.constrsubstl σ c is a short-hand for substnl σ 0 c
val subst1 : Constr.constr -> Constr.constr -> Constr.constrsubstl a c is a short-hand for substnl [a] 0 c
val substnl_decl :
substl ->
int ->
Constr.rel_declaration ->
Constr.rel_declarationsubstnl_decl [a₁;...;an] k Ω substitutes in parallel a₁, ..., an for respectively Rel(k+1), ..., Rel(k+n) in a declaration Ω; it relocates accordingly indexes in a₁,...,an and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=k, then Γ, Γ', substnl_decl [a₁;...;an] k Ω ⊢.
val substl_decl : substl -> Constr.rel_declaration -> Constr.rel_declarationsubstl_decl σ Ω is a short-hand for substnl_decl σ 0 Ω
val subst1_decl :
Constr.constr ->
Constr.rel_declaration ->
Constr.rel_declarationsubst1_decl a Ω is a short-hand for substnl_decl [a] 0 Ω
val substnl_rel_context :
substl ->
int ->
Constr.rel_context ->
Constr.rel_contextsubstnl_rel_context [a₁;...;an] k Ω substitutes in parallel a₁, ..., an for respectively Rel(k+1), ..., Rel(k+n) in a context Ω; it relocates accordingly indexes in a₁,...,an and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=k, then Γ, Γ', substnl_rel_context [a₁;...;an] k Ω ⊢.
val substl_rel_context : substl -> Constr.rel_context -> Constr.rel_contextsubstl_rel_context σ Ω is a short-hand for substnl_rel_context σ 0 Ω
val subst1_rel_context :
Constr.constr ->
Constr.rel_context ->
Constr.rel_contextsubst1_rel_context a Ω is a short-hand for substnl_rel_context [a] 0 Ω
val esubst :
( int -> 'a -> Constr.constr ) ->
'a Esubst.subs ->
Constr.constr ->
Constr.constresubst lift σ c substitutes c with arbitrary complex substitution σ, using lift to lift subterms where necessary.
val replace_vars :
(Names.Id.t * Constr.constr) list ->
Constr.constr ->
Constr.constrreplace_vars k [(id₁,c₁);...;(idn,cn)] t substitutes Var idj by cj in t.
val substn_vars : int -> Names.Id.t list -> Constr.constr -> Constr.constrsubstn_vars k [id₁;...;idn] t substitutes Var idj by Rel j+k-1 in t. If two names are identical, the one of least index is kept. In terms of typing, if Γ,xn:Un,...,x₁:U₁,Γ' ⊢ t:T, together with idj:Tj and Γ,xn:Un,...,x₁:U₁,Γ' ⊢ Tj[idj+1..idn:=xj+1..xn] ≡ Uj, then Γ\{id₁,...,idn},xn:Un,...,x₁:U₁,Γ' ⊢ substn_vars
(|Γ'|+1) [id₁;...;idn] t : substn_vars (|Γ'|+1) [id₁;...;idn]
T.
val subst_vars : Names.Id.t list -> Constr.constr -> Constr.constrsubst_vars [id1;...;idn] t is a short-hand for substn_vars
[id1;...;idn] 1 t: it substitutes Var idj by Rel j in t. If two names are identical, the one of least index is kept.
val subst_var : Names.Id.t -> Constr.constr -> Constr.constrsubst_var id t is a short-hand for substn_vars [id] 1 t: it substitutes Var id by Rel 1 in t.
val smash_rel_context : Constr.rel_context -> Constr.rel_contextExpand lets in context
Level substitutions for polymorphism.
val subst_univs_level_constr :
Univ.universe_level_subst ->
Constr.constr ->
Constr.constrval subst_univs_level_context :
Univ.universe_level_subst ->
Constr.rel_context ->
Constr.rel_contextval subst_instance_constr : Univ.Instance.t -> Constr.constr -> Constr.constrInstance substitution for polymorphism.
val subst_instance_context :
Univ.Instance.t ->
Constr.rel_context ->
Constr.rel_contextval univ_instantiate_constr :
Univ.Instance.t ->
Constr.constr Univ.univ_abstracted ->
Constr.constrIgnores the constraints carried by univ_abstracted.
val universes_of_constr : Constr.constr -> Univ.Level.Set.tval make_substituend : Constr.constr -> substituendval lift_substituend : int -> substituend -> Constr.constr