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

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

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

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

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

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 Ω ⊢.

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

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

Level substitutions for polymorphism.

val subst_univs_level_constr : UVars.sort_level_subst -> Constr.constr -> Constr.constr
val subst_univs_level_context : UVars.sort_level_subst -> Constr.rel_context -> Constr.rel_context
val subst_instance_constr : UVars.Instance.t -> Constr.constr -> Constr.constr

Instance substitution for polymorphism.

val subst_instance_context : UVars.Instance.t -> Constr.rel_context -> Constr.rel_context

Ignores the constraints carried by univ_abstracted.

val map_constr_relevance : (Sorts.relevance -> Sorts.relevance) -> Constr.t -> Constr.t

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

val sort_and_universes_of_constr : ?init:(Sorts.QVar.Set.t * Univ.Level.Set.t) -> Constr.constr -> Sorts.QVar.Set.t * Univ.Level.Set.t
val universes_of_constr : ?init:Univ.Level.Set.t -> Constr.constr -> Univ.Level.Set.t
type ('a, 's, 'u, 'r) univ_visitor = {
visit_sort : 'a -> 's -> 'a;
visit_instance : 'a -> 'u -> 'a;
visit_relevance : 'a -> 'r -> 'a;
}
val visit_kind_univs : ('acc'sort'instance'relevance) univ_visitor -> 'acc -> (__'sort'instance'relevance) Constr.kind_of_term -> 'acc

Low-level cached lift type

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