package coq

  1. Overview
  2. Docs
Package contains no libraries
type !'a red_atom =
  1. | FBeta
  2. | FMatch
  3. | FFix
  4. | FCofix
  5. | FZeta
  6. | FConst of 'a list
  7. | FDeltaBut of 'a list
type !'a glob_red_flag = {
  1. rBeta : bool;
  2. rMatch : bool;
  3. rFix : bool;
  4. rCofix : bool;
  5. rZeta : bool;
  6. rDelta : bool;
  7. rConst : 'a list;
}
type (!'a, !'b, !'c) red_expr_gen =
  1. | Red of bool
  2. | Hnf
  3. | Simpl of 'b glob_red_flag * ('b, 'c) Util.union Locus.with_occurrences option
  4. | Cbv of 'b glob_red_flag
  5. | Cbn of 'b glob_red_flag
  6. | Lazy of 'b glob_red_flag
  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) may_eval =
  1. | ConstrTerm of 'a
  2. | ConstrEval of ('a, 'b, 'c) red_expr_gen * 'a
  3. | ConstrContext of Names.Id.t Loc.located * 'a
  4. | ConstrTypeOf of 'a
type raw_red_expr = (r_trm, r_cst, r_pat) 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