coq-core 8.18.0 · OCaml Package

Derived constructors

val mkArrow : Constr.types -> Sorts.relevance -> Constr.types -> Constr.constr

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

val mkArrowR : Constr.types -> Constr.types -> Constr.constr

For an always-relevant domain

val mkNamedLambda : 
  Names.Id.t Context.binder_annot ->
  Constr.types ->
  Constr.constr ->
  Constr.constr

Named version of the functions from Term.

val mkNamedLetIn : 
  Names.Id.t Context.binder_annot ->
  Constr.constr ->
  Constr.types ->
  Constr.constr ->
  Constr.constr

val mkNamedProd : 
  Names.Id.t Context.binder_annot ->
  Constr.types ->
  Constr.types ->
  Constr.types

val mkProd_or_LetIn : Constr.rel_declaration -> Constr.types -> Constr.types

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

val mkProd_wo_LetIn : Constr.rel_declaration -> Constr.types -> Constr.types

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

val prodn : 
  int ->
  (Names.Name.t Context.binder_annot * Constr.constr) list ->
  Constr.constr ->
  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)....

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

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.

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

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

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

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_decls : 
  int ->
  Constr.constr ->
  Constr.constr list ->
  Constr.constr

In lambda_applist_decls 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_decls : 
  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_decls : 
  int ->
  Constr.types ->
  Constr.constr array ->
  Constr.types

In prod_appvect_decls 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_decls : 
  int ->
  Constr.types ->
  Constr.constr list ->
  Constr.types

Other term destructors.

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

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.

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

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.

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

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_decls : 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_lambda_decls : 
  Constr.constr ->
  Constr.rel_context * Constr.constr

Idem with lambda's and let's

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

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

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

Idem for lambdas, _not_ counting let-ins

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

Idem, counting let-ins

val prod_decls : Constr.types -> Constr.rel_context

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

val lambda_decls : Constr.constr -> Constr.rel_context

val prod_n_decls : 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_decls : Constr.types -> Constr.types

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

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

type arity = Constr.rel_context * Sorts.t

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 =

| InSProp
| InProp
| InSet
| InType
| InQSort

deprecated Alias for Sorts.family

type sorts = private Sorts.t =

| SProp
| Prop
| Set
| Type of Univ.Universe.t
(*
Type
*)
| QSort of Sorts.QVar.t * Univ.Universe.t

deprecated Alias for Sorts.t

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

deprecated Use [decompose_prod_decls] instead.

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

deprecated Use [decompose_lambda_decls] instead.

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

deprecated Use [decompose_prod_n_decls] instead.

val prod_assum : Constr.types -> Constr.rel_context

deprecated Use [prod_decls] instead.

val lam_assum : Constr.constr -> Constr.rel_context

deprecated Use [lambda_decls] instead.

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

deprecated Use [prod_n_decls] instead.

val strip_prod_assum : Constr.types -> Constr.types

deprecated Use [strip_prod_decls] instead.

val strip_lam_assum : Constr.constr -> Constr.constr

deprecated Use [strip_lambda_decls] instead.

val decompose_lam : 
  Constr.t ->
  (Names.Name.t Context.binder_annot * Constr.t) list * Constr.t

deprecated Use [decompose_lambda] instead.

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

deprecated Use [decompose_lambda_n] instead.

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

deprecated Use [decompose_lambda_n_assum] instead.

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

deprecated Use [decompose_lambda_n_decls] instead.

package coq-core

Derived constructors

Other term constructors.

Other term destructors.

...