package coq-core
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
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