package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.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
type 'a glob_red_flag = {rStrength : strength;rBeta : bool;rMatch : bool;rFix : bool;rCofix : bool;rZeta : bool;rDelta : bool;(*true = delta all but rConst; false = delta only on rConst
*)rConst : 'a list;
}Generic kinds of reductions
type ('b, 'c, 'occvar) red_context =
('occvar Locus.occurrences_gen * ('b, 'c) Util.union) optiontype ('a, 'b, 'c, 'occvar, 'flags) red_expr_gen0 = | Red| Hnf| Simpl of 'flags * ('b, 'c, 'occvar) red_context| Cbv of 'flags| Cbn of 'flags| Lazy of 'flags| Unfold of ('occvar Locus.occurrences_gen * 'b) list| Fold of 'a list| Pattern of ('occvar Locus.occurrences_gen * 'a) list| ExtraRedExpr of string| CbvVm of ('b, 'c, 'occvar) red_context| CbvNative of ('b, 'c, 'occvar) red_context
type ('a, 'b, 'c, 'occvar) red_expr_gen =
('a, 'b, 'c, 'occvar, 'b glob_red_flag) red_expr_gen0type ('a, 'b, 'c, 'occvar) may_eval = | ConstrTerm of 'a| ConstrEval of ('a, 'b, 'c, 'occvar) 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, int Locus.or_var) red_expr_gentype 'a and_short_name = 'a * Names.lident optiontype g_trm = Genintern.glob_constr_and_exprtype g_pat = Genintern.glob_constr_pattern_and_exprtype g_cst = Evaluable.t and_short_name Locus.or_vartype glob_red_expr = (g_trm, g_cst, g_trm, int Locus.or_var) red_expr_gen