package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz

md5=13d2793fc6413aac5168822313e4864e

sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/coq-core.tactics/Genredexpr/index.html

Module `Genredexpr`

Reduction expressions

The parsing produces initially a list of red_atom

type 'a red_atom =

| FBeta
| FMatch
| FFix
| FCofix
| FZeta
| FConst of 'a list
| FDeltaBut of 'a list
| FHead

This list of atoms is immediately converted to a glob_red_flag

type strength =

| Norm
| Head

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 ('a, 'b, 'c, 'flags) red_expr_gen0 =

| Red
| 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_gen0

type ('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_expr

type r_pat = Constrexpr.constr_pattern_expr

type r_cst = Libnames.qualid Constrexpr.or_by_notation

type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen

type 'a and_short_name = 'a * Names.lident option

type g_trm = Genintern.glob_constr_and_expr

type g_pat = Genintern.glob_constr_pattern_and_expr

type g_cst = Tacred.evaluable_global_reference and_short_name Locus.or_var

type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen