package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.pretyping/Cbv/index.html
Module CbvSource
Entry point for cbv normalization of a constr
Source
type cbv_value = | VAL of int * Constr.constr| STACK of int * cbv_value * cbv_stack| CBN of Constr.constr * cbv_value Esubst.subs| LAM of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * cbv_value Esubst.subs| FIXP of Constr.fixpoint * cbv_value Esubst.subs * cbv_value array| COFIXP of Constr.cofixpoint * cbv_value Esubst.subs * cbv_value array| CONSTR of Names.constructor Univ.puniverses * cbv_value array| PRIMITIVE of CPrimitives.t * Constr.pconstant * cbv_value array| ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value
Source
and cbv_stack = | TOP| APP of cbv_value list * cbv_stack| CASE of Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * Constr.case_invert * Constr.case_info * cbv_value Esubst.subs * cbv_stack| PROJ of Names.Projection.t * cbv_stack
Source
val cbv_stack_term :
cbv_infos ->
cbv_stack ->
cbv_value Esubst.subs ->
Constr.constr ->
cbv_valuerecursive functions...
Source
val norm_head :
cbv_infos ->
cbv_value Esubst.subs ->
Constr.constr ->
cbv_stack ->
cbv_value * cbv_stackEnd of cbv debug section i