package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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

Module Genredexpr

Reduction expressions

The parsing produces initially a list of red_atom

type 'a red_atom =
  1. | FBeta
  2. | FMatch
  3. | FFix
  4. | FCofix
  5. | FZeta
  6. | FConst of 'a list
  7. | FDeltaBut of 'a list
  8. | FHead

This list of atoms is immediately converted to a glob_red_flag

type strength =
  1. | Norm
  2. | Head
type 'a glob_red_flag = {
  1. rStrength : strength;
  2. rBeta : bool;
  3. rMatch : bool;
  4. rFix : bool;
  5. rCofix : bool;
  6. rZeta : bool;
  7. rDelta : bool;
    (*

    true = delta all but rConst; false = delta only on rConst

    *)
  8. rConst : 'a list;
}

Generic kinds of reductions

type ('b, 'c, 'occvar) red_context = ('occvar Locus.occurrences_gen * ('b, 'c) Util.union) option
type ('a, 'b, 'c, 'occvar, 'flags) red_expr_gen0 =
  1. | Red
  2. | Hnf
  3. | Simpl of 'flags * ('b, 'c, 'occvar) red_context
  4. | Cbv of 'flags
  5. | Cbn of 'flags
  6. | Lazy of 'flags
  7. | Unfold of ('occvar Locus.occurrences_gen * 'b) list
  8. | Fold of 'a list
  9. | Pattern of ('occvar Locus.occurrences_gen * 'a) list
  10. | ExtraRedExpr of string
  11. | CbvVm of ('b, 'c, 'occvar) red_context
  12. | 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_gen0
type ('a, 'b, 'c, 'occvar) may_eval =
  1. | ConstrTerm of 'a
  2. | ConstrEval of ('a, 'b, 'c, 'occvar) red_expr_gen * 'a
  3. | ConstrContext of Names.lident * 'a
  4. | ConstrTypeOf of 'a
type raw_red_expr = (r_trm, r_cst, r_pat, int Locus.or_var) red_expr_gen
type 'a and_short_name = 'a * Names.lident option
type glob_red_expr = (g_trm, g_cst, g_trm, int Locus.or_var) red_expr_gen