package coq

  1. Overview
  2. Docs
package coq
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

This list of atoms is immediately converted to a glob_red_flag

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

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

    *)
  7. rConst : 'a list;
}

Generic kinds of reductions

type ('a, 'b, 'c, 'flags) red_expr_gen0 =
  1. | Red of bool
  2. | Hnf
  3. | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option
  4. | Cbv of 'flags
  5. | Cbn of 'flags
  6. | Lazy of 'flags
  7. | Unfold of 'b Locus.with_occurrences list
  8. | Fold of 'a list
  9. | Pattern of 'a Locus.with_occurrences list
  10. | ExtraRedExpr of string
  11. | CbvVm of ('b, 'c) Util.union Locus.with_occurrences option
  12. | 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 =
  1. | ConstrTerm of 'a
  2. | ConstrEval of ('a, 'b, 'c) red_expr_gen * 'a
  3. | ConstrContext of Names.lident * 'a
  4. | ConstrTypeOf of 'a
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
val make0 : ?dyn:'a Geninterp.Val.tag -> string -> ('b, 'c, 'd) Genarg.genarg_type
type 'a and_short_name = 'a * Names.lident option
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