Module Vars

Occur checks
val closedn : int -> Constr.constr -> bool

closedn n M is true iff M is a (de Bruijn) closed term under n binders

val closed0 : Constr.constr -> bool

closed0 M is true iff M is a (de Bruijn) closed term

val noccurn : int -> Constr.constr -> bool

noccurn n M returns true iff Rel n does NOT occur in term M

val noccur_between : int -> int -> Constr.constr -> bool

noccur_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 -> bool

Checking 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)

Relocation and substitution
val exliftn : Esubst.lift -> Constr.constr -> Constr.constr

exliftn el c lifts c with arbitrary complex lifting el

val liftn : int -> int -> Constr.constr -> Constr.constr

liftn n k c lifts by n indexes above 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.constr

lift n c lifts by n the positive indexes in c

val liftn_rel_context : int -> int -> Constr.rel_context -> Constr.rel_context

Same as liftn for a context

val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context

Same as lift for a context

type substl = Constr.constr list
type instance = Constr.constr array
type instance_list = Constr.constr list
val subst_of_rel_context_instance : Constr.rel_context -> instance -> substl

Let Γ 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 -> substl
val adjust_rel_to_rel_context : ('a'b) Context.Rel.pt -> int -> int

Take 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.constr

substnl [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.constr

substl σ c is a short-hand for substnl σ 0 c

val subst1 : Constr.constr -> Constr.constr -> Constr.constr

substl a c is a short-hand for substnl [a] 0 c

val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration

substnl_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_declaration

substl_decl σ Ω is a short-hand for substnl_decl σ 0 Ω

val subst1_decl : Constr.constr -> Constr.rel_declaration -> Constr.rel_declaration

subst1_decl a Ω is a short-hand for substnl_decl [a] 0 Ω

val substnl_rel_context : substl -> int -> Constr.rel_context -> Constr.rel_context

substnl_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_context

substl_rel_context σ Ω is a short-hand for substnl_rel_context σ 0 Ω

val subst1_rel_context : Constr.constr -> Constr.rel_context -> Constr.rel_context

subst1_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.constr

esubst 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.constr

replace_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.constr

substn_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.constr

subst_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.constr

subst_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_context

Expand lets in context

Substitution of universes

val subst_univs_level_constr : Univ.universe_level_subst -> Constr.constr -> Constr.constr
val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context -> Constr.rel_context
val subst_instance_constr : Univ.Instance.t -> Constr.constr -> Constr.constr

Instance substitution for polymorphism.

val subst_instance_context : Univ.Instance.t -> Constr.rel_context -> Constr.rel_context
val univ_instantiate_constr : Univ.Instance.t -> Constr.constr Univ.univ_abstracted -> Constr.constr

Ignores the constraints carried by univ_abstracted.

val universes_of_constr : Constr.constr -> Univ.Level.Set.t

Low-level cached lift type

type substituend
val make_substituend : Constr.constr -> substituend
val lift_substituend : int -> substituend -> Constr.constr