package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 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

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

lift n c lifts by n the positive indexes in c

The type substl is the type of substitutions u₁..un of type some 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₁].

type substl = Constr.constr list
val subst_of_rel_context_instance : Constr.rel_context -> Constr.constr list -> 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 Γ 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 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.

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

Substitution of universes

Level substitutions for polymorphism.

val subst_univs_level_constr : Univ.universe_level_subst -> Constr.constr -> Constr.constr
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

Ignores the constraints carried by univ_abstracted.

val universes_of_constr : Constr.constr -> Univ.LSet.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct