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`