# Module Vars

###### Occur checks
val closedn : int -> bool

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

val closed0 : bool

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

val noccurn : int -> bool

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

val noccur_between : int -> int -> 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 -> 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 : Constr.constr

exliftn el c lifts c with arbitrary complex lifting el

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

liftn 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

lift n c lifts by n the positive indexes in c

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

Same as liftn for a context

val lift_rel_context : int -> Constr.rel_context

Same 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:

• Γ ⊢ ∅ : ∅,
• Γ ⊢ u₁..un-1 : Δ and Γ ⊢ un : An[u₁..un-1] implies Γ ⊢ u₁..un : Δ,xn:An
• Γ ⊢ u₁..un-1 : Δ and Γ ⊢ un : An[u₁..un-1] implies Γ ⊢ u₁..un : Δ,xn:=cn:An when Γ ⊢ un ≡ cn[u₁..un-1]

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 list

The 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₁..un : Δ and Γ ⊢ un+1 : An+1[ϕ(Δ,u₁..un)] implies Γ ⊢ u₁..un+1 : Δ,xn+1:An+1
• Γ ⊢ u₁..un : Δ implies Γ ⊢ u₁..un : Δ,xn+1:=cn+1:An+1 where ϕ(Δ,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 array
type instance_list = Constr.constr list
val subst_of_rel_context_instance : 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 : substl
val adjust_rel_to_rel_context : ('a'b'r) 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

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

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

val subst1 : Constr.constr

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

val substnl_decl : substl -> int -> 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

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

val subst1_decl : Constr.rel_declaration

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

val substnl_rel_context : substl -> int -> 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

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

val subst1_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) -> -> Constr.constr

esubst lift σ c substitutes c with arbitrary complex substitution σ, using lift to lift subterms where necessary.

val replace_vars : list -> 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

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

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 : 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

Expand lets in context

#### Substitution of universes

Level substitutions for polymorphism.

val subst_univs_level_constr : Constr.constr
val subst_univs_level_context : Constr.rel_context
val subst_instance_constr : Constr.constr

Instance substitution for polymorphism.

val subst_instance_context : Constr.rel_context
val univ_instantiate_constr : Constr.constr

Ignores the constraints carried by univ_abstracted.

val map_constr_relevance : -> Constr.t -> Constr.t

Modifies the relevances in the head node (not in subterms)

val sort_and_universes_of_constr : Sorts.QVar.Set.t * Univ.Level.Set.t
val universes_of_constr : Univ.Level.Set.t

#### Low-level cached lift type

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