package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.tactics/Genredexpr/index.html
Module Genredexpr
Reduction expressions
The parsing produces initially a list of red_atom
This list of atoms is immediately converted to a glob_red_flag
Generic kinds of reductions
type ('a, 'b, 'c, 'flags) red_expr_gen0 = | Red of bool| Hnf| Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option| Cbv of 'flags| Cbn of 'flags| Lazy of 'flags| Unfold of 'b Locus.with_occurrences list| Fold of 'a list| Pattern of 'a Locus.with_occurrences list| ExtraRedExpr of string| CbvVm of ('b, 'c) Util.union Locus.with_occurrences option| CbvNative of ('b, 'c) Util.union Locus.with_occurrences option
type ('a, 'b, 'c) red_expr_gen = ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0type ('a, 'b, 'c) may_eval = | ConstrTerm of 'a| ConstrEval of ('a, 'b, 'c) red_expr_gen * 'a| ConstrContext of Names.lident * 'a| ConstrTypeOf of 'a
type r_trm = Constrexpr.constr_exprtype r_pat = Constrexpr.constr_pattern_exprtype r_cst = Libnames.qualid Constrexpr.or_by_notationtype raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gentype 'a and_short_name = 'a * Names.lident option