package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.kernel/Term/index.html
Module TermSource
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
val mkNamedLambda :
Names.Id.t Constr.binder_annot ->
Constr.types ->
Constr.constr ->
Constr.constrNamed version of the functions from Term.
val mkNamedLetIn :
Names.Id.t Constr.binder_annot ->
Constr.constr ->
Constr.types ->
Constr.constr ->
Constr.constrval mkNamedProd :
Names.Id.t Constr.binder_annot ->
Constr.types ->
Constr.types ->
Constr.typesConstructs either (x:t)c or [x=b:t]c
Constructs either [x:t]c or [x=b:t]c
Other term constructors.
applist (f,args) and its variants work as mkApp
val prodn :
int ->
(Names.Name.t Constr.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrprodn 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 Constr.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrcompose_prod l b
val lamn :
int ->
(Names.Name.t Constr.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrlamn n l b
val compose_lam :
(Names.Name.t Constr.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrcompose_lam l b
to_lambda n l
to_prod n l
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.
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.
pseudo-reduction rule
prod_appvect forall (x1:B1;...;xn:Bn), B a1...an
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.
Other term destructors.
val decompose_prod :
Constr.constr ->
(Names.Name.t Constr.binder_annot * Constr.constr) list * Constr.constrTransforms 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 Constr.binder_annot * Constr.constr) list * Constr.constrTransforms 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 Constr.binder_annot * Constr.constr) list * Constr.constrGiven 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 Constr.binder_annot * Constr.constr) list * Constr.constrGiven 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.
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
Idem with lambda's and let's
Idem but extract the first n premisses, counting let-ins.
val decompose_lambda_prod_n_decls :
int ->
Constr.constr ->
Constr.types ->
Constr.rel_context * Constr.constr * Constr.typesIdem but extracting simultaneously the first n premisses, counting let-ins, in a term and its type.
Idem for lambdas, including let-ins but _not_ counting them; This is typically the function to use to extract the context of a Fix up to and including the decreasing argument, counting as many lambda's as given by the decreasing index + 1
Idem, counting let-ins
Return the premisses/parameters of a type/term (let-in included)
Return the first n-th premisses/parameters of a type (let included and counted)
Return the first n-th premisses/parameters of a term (let included but not counted)
Remove the premisses/parameters of a type/term
Remove the first n-th premisses/parameters of a type/term
Remove the premisses/parameters of a type/term (including let-in)
...
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
Build an "arity" from its canonical form
Destruct an "arity" into its canonical form
Tell if a term has the form of an arity
type sorts = private Sorts.t = | SProp| Prop| Set| Type of Univ.Universe.t(*Type
*)| QSort of Sorts.QVar.t * Univ.Universe.t
val decompose_lam_n :
int ->
Constr.t ->
(Names.Name.t Constr.binder_annot * Constr.t) list * Constr.t