package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
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