package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
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 Context.binder_annot ->
Constr.types ->
Constr.constr ->
Constr.constrNamed version of the functions from Term.
val mkNamedLetIn :
Names.Id.t Context.binder_annot ->
Constr.constr ->
Constr.types ->
Constr.constr ->
Constr.constrval mkNamedProd :
Names.Id.t Context.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 Context.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 Context.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrcompose_prod l b
val lamn :
int ->
(Names.Name.t Context.binder_annot * Constr.constr) list ->
Constr.constr ->
Constr.constrlamn n l b
val compose_lam :
(Names.Name.t Context.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_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.
pseudo-reduction rule
prod_appvect forall (x1:B1;...;xn:Bn), B a1...an
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.
Other term destructors.
val decompose_prod :
Constr.constr ->
(Names.Name.t Context.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_lam :
Constr.constr ->
(Names.Name.t Context.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 Context.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_lam_n :
int ->
Constr.constr ->
(Names.Name.t Context.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.
Idem for lambdas, _not_ counting let-ins
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