package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type universe_decl_expr = (Names.lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
type ident_decl = Names.lident * universe_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
type notation_entry_level =
  1. | InConstrEntrySomeLevel
  2. | InCustomEntryLevel of string * int
type notation_key = string
type !'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
type !'a or_by_notation = 'a or_by_notation_r CAst.t
type explicitation =
  1. | ExplByPos of int * Names.Id.t option
  2. | ExplByName of Names.Id.t
type binder_kind =
  1. | Default of Glob_term.binding_kind
  2. | Generalized of Glob_term.binding_kind * bool
type abstraction_kind =
  1. | AbsLambda
  2. | AbsPi
type proj_flag = int option
type sign =
  1. | SPlus
  2. | SMinus
type raw_numeral = NumTok.t
type prim_token =
  1. | Numeral of sign * raw_numeral
  2. | String of string
type instance_expr = Glob_term.glob_level list
type cases_pattern_expr_r =
  1. | CPatAlias of cases_pattern_expr * Names.lname
  2. | CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list
  3. | CPatAtom of Libnames.qualid option
  4. | CPatOr of cases_pattern_expr list
  5. | CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list
  6. | CPatPrim of prim_token
  7. | CPatRecord of (Libnames.qualid * cases_pattern_expr) list
  8. | CPatDelimiters of string * cases_pattern_expr
  9. | CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
and cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list
and constr_expr_r =
  1. | CRef of Libnames.qualid * instance_expr option
  2. | CFix of Names.lident * fix_expr list
  3. | CCoFix of Names.lident * cofix_expr list
  4. | CProdN of local_binder_expr list * constr_expr
  5. | CLambdaN of local_binder_expr list * constr_expr
  6. | CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
  7. | CAppExpl of proj_flag * Libnames.qualid * instance_expr option * constr_expr list
  8. | CApp of proj_flag * constr_expr * (constr_expr * explicitation CAst.t option) list
  9. | CRecord of (Libnames.qualid * constr_expr) list
  10. | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
  11. | CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
  12. | CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
  13. | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
  14. | CPatVar of Pattern.patvar
  15. | CEvar of Glob_term.existential_name * (Names.Id.t * constr_expr) list
  16. | CSort of Glob_term.glob_sort
  17. | CCast of constr_expr * constr_expr Glob_term.cast_type
  18. | CNotation of notation * constr_notation_substitution
  19. | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
  20. | CPrim of prim_token
  21. | CDelimiters of string * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr * Names.lname option * cases_pattern_expr option
and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t
and recursion_order_expr_r =
  1. | CStructRec of Names.lident
  2. | CWfRec of Names.lident * constr_expr
  3. | CMeasureRec of Names.lident option * constr_expr * constr_expr option
and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
  1. | CLocalAssum of Names.lname list * binder_kind * constr_expr
  2. | CLocalDef of Names.lname * constr_expr * constr_expr option
  3. | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
and constr_notation_substitution = constr_expr list * constr_expr list list * cases_pattern_expr list * local_binder_expr list list
type constr_pattern_expr = constr_expr
type with_declaration_ast =
  1. | CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
  2. | CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
  1. | CMident of Libnames.qualid
  2. | CMapply of module_ast * module_ast
  3. | CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t
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