package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct