package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Derived constructors

non-dependent product t1 -> t2, an alias for forall (_:t1), t2. Beware t_2 is NOT lifted. Eg: in context A:Prop, A->A is built by (mkArrow (mkRel 1) (mkRel 2))

For an always-relevant domain

Named version of the functions from Term.

Constructs either (x:t)c or [x=b:t]c

val mkNamedProd_or_LetIn : Constr.named_declaration -> Constr.types -> Constr.types
val mkNamedProd_wo_LetIn : Constr.named_declaration -> Constr.types -> Constr.types
val mkLambda_or_LetIn : Constr.rel_declaration -> Constr.constr -> Constr.constr

Constructs either [x:t]c or [x=b:t]c

val mkNamedLambda_or_LetIn : Constr.named_declaration -> Constr.constr -> Constr.constr
Other term constructors.

applist (f,args) and its variants work as mkApp

val applist : (Constr.constr * Constr.constr list) -> Constr.constr
val applistc : Constr.constr -> Constr.constr list -> Constr.constr
val appvect : (Constr.constr * Constr.constr array) -> Constr.constr
val appvectc : Constr.constr -> Constr.constr array -> Constr.constr

prodn n l b = forall (x_1:T_1)...(x_n:T_n), b where l is (x_n,T_n)...(x_1,T_1)....

compose_prod l b

  • returns

    forall (x_1:T_1)...(x_n:T_n), b where l is (x_n,T_n)...(x_1,T_1). Inverse of decompose_prod.

lamn n l b

  • returns

    fun (x_1:T_1)...(x_n:T_n) => b where l is (x_n,T_n)...(x_1,T_1)....

compose_lam l b

  • returns

    fun (x_1:T_1)...(x_n:T_n) => b where l is (x_n,T_n)...(x_1,T_1). Inverse of it_destLam

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

to_lambda n l

  • returns

    fun (x_1:T_1)...(x_n:T_n) => T where l is forall (x_1:T_1)...(x_n:T_n), T

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

to_prod n l

  • returns

    forall (x_1:T_1)...(x_n:T_n), T where l is fun (x_1:T_1)...(x_n:T_n) => T

val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val it_mkProd_wo_LetIn : Constr.types -> Constr.rel_context -> Constr.types
val it_mkProd_or_LetIn : Constr.types -> Constr.rel_context -> Constr.types
val lambda_applist : Constr.constr -> Constr.constr list -> Constr.constr

In lambda_applist c args, c is supposed to have the form λΓ.c with Γ without let-in; it returns c with the variables of Γ instantiated by args.

val lambda_appvect : Constr.constr -> Constr.constr array -> Constr.constr
val lambda_applist_assum : int -> Constr.constr -> Constr.constr list -> Constr.constr

In lambda_applist_assum n c args, c is supposed to have the form λΓ.c with Γ of length n and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

val lambda_appvect_assum : int -> Constr.constr -> Constr.constr array -> Constr.constr

pseudo-reduction rule

val prod_appvect : Constr.types -> Constr.constr array -> Constr.types

prod_appvect forall (x1:B1;...;xn:Bn), B a1...an

  • returns

    B[a1...an]

val prod_applist : Constr.types -> Constr.constr list -> Constr.types
val prod_appvect_assum : int -> Constr.types -> Constr.constr array -> Constr.types

In prod_appvect_assum n c args, c is supposed to have the form ∀Γ.c with Γ of length n and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

val prod_applist_assum : int -> Constr.types -> Constr.constr list -> Constr.types
Other term destructors.

Transforms a product term $ (x_1:T_1)..(x_n:T_n)T $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ , where $ T $ is not a product.

Transforms a lambda term $ x_1:T_1..x_n:T_nT $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ , where $ T $ is not a lambda.

val decompose_prod_n : int -> Constr.constr -> (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr

Given a positive integer n, decompose a product term $ (x_1:T_1)..(x_n:T_n)T $ into the pair $ ((xn,Tn);...;(x1,T1),T) $ . Raise a user error if not enough products.

Given a positive integer $ n $ , decompose a lambda term $ x_1:T_1..x_n:T_nT $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ . Raise a user error if not enough lambdas.

val decompose_prod_assum : Constr.types -> Constr.rel_context * Constr.types

Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let

val decompose_lam_assum : Constr.constr -> Constr.rel_context * Constr.constr

Idem with lambda's and let's

val decompose_prod_n_assum : int -> Constr.types -> Constr.rel_context * Constr.types

Idem but extract the first n premisses, counting let-ins.

val decompose_lam_n_assum : int -> Constr.constr -> Constr.rel_context * Constr.constr

Idem for lambdas, _not_ counting let-ins

val decompose_lam_n_decls : int -> Constr.constr -> Constr.rel_context * Constr.constr

Idem, counting let-ins

val prod_assum : Constr.types -> Constr.rel_context

Return the premisses/parameters of a type/term (let-in included)

val prod_n_assum : int -> Constr.types -> Constr.rel_context

Return the first n-th premisses/parameters of a type (let included and counted)

val lam_n_assum : int -> Constr.constr -> Constr.rel_context

Return the first n-th premisses/parameters of a term (let included but not counted)

val strip_prod : Constr.types -> Constr.types

Remove the premisses/parameters of a type/term

val strip_lam : Constr.constr -> Constr.constr
val strip_prod_n : int -> Constr.types -> Constr.types

Remove the first n-th premisses/parameters of a type/term

val strip_lam_n : int -> Constr.constr -> Constr.constr
val strip_prod_assum : Constr.types -> Constr.types

Remove the premisses/parameters of a type/term (including let-in)

val strip_lam_assum : Constr.constr -> Constr.constr
...

An "arity" is a term of the form [x1:T1]...[xn:Tn]s with s a sort. Such a term can canonically be seen as the pair of a context of types and of a sort

val mkArity : arity -> Constr.types

Build an "arity" from its canonical form

val destArity : Constr.types -> arity

Destruct an "arity" into its canonical form

val isArity : Constr.types -> bool

Tell if a term has the form of an arity

type sorts_family = Sorts.family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
  • deprecated Alias for Sorts.family
type sorts = private Sorts.t =
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
    (*

    Type

    *)
  • deprecated Alias for Sorts.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