package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Concrete syntax for terms
type sort_name_expr =
  1. | CSProp
  2. | CProp
  3. | CSet
  4. | CType of Libnames.qualid
  5. | CRawType of Univ.Level.t
    (*

    Universes like "foo.1" have no qualid form

    *)

Universes

type sort_expr = (Sorts.QVar.t option * (sort_name_expr * int) list) Glob_term.glob_sort_gen
type instance_expr = univ_level_expr list
type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr

Constraints don't have anonymous universes

type universe_decl_expr = (Names.lident list, univ_constraint_expr list) UState.gen_universe_decl
type cumul_univ_decl_expr = ((Names.lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
type ident_decl = Names.lident * universe_decl_expr option
type cumul_ident_decl = Names.lident * cumul_univ_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_with_optional_scope =
  1. | LastLonelyNotation
  2. | NotationInScope of string
type side =
  1. | Left
  2. | Right
type entry_level = int
type entry_relative_level =
  1. | LevelLt of entry_level
  2. | LevelLe of entry_level
  3. | LevelSome
type notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
type notation_entry_level = notation_entry * entry_level
type notation_entry_relative_level = notation_entry * (entry_relative_level * side option)
type notation_key = string
type notation = notation_entry * notation_key
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. | ExplByName of Names.Id.t
  2. | ExplByPos of int
type binder_kind =
  1. | Default of Glob_term.binding_kind
  2. | Generalized of Glob_term.binding_kind * bool
    (*

    (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses

    *)
type explicit_flag = bool

true = with "@"

type prim_token =
  1. | Number of NumTok.Signed.t
  2. | String of string
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
    (*

    CPatCstr (_, c, Some l1, l2) represents (@ c l1) l2

    *)
  3. | CPatAtom of Libnames.qualid option
  4. | CPatOr of cases_pattern_expr list
  5. | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list
    (*

    CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2

    *)
  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

constr_expr is the abstract syntax tree produced by the parser

and cases_pattern_expr = cases_pattern_expr_r CAst.t
and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
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 Libnames.qualid * instance_expr option * constr_expr list
  8. | CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
  9. | CProj of explicit_flag * Libnames.qualid * instance_expr option * (constr_expr * explicitation CAst.t option) list * constr_expr
  10. | CRecord of (Libnames.qualid * constr_expr) list
  11. | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
  12. | CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
  13. | CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
  14. | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr
  15. | CGenarg of Genarg.raw_generic_argument
  16. | CGenargGlob of Genarg.glob_generic_argument
  17. | CPatVar of Pattern.patvar
  18. | CEvar of Glob_term.existential_name CAst.t * (Names.lident * constr_expr) list
  19. | CSort of sort_expr
  20. | CCast of constr_expr * Constr.cast_kind option * constr_expr
  21. | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
  22. | CGeneralization of Glob_term.binding_kind * constr_expr
  23. | CPrim of prim_token
  24. | CDelimiters of string * constr_expr
  25. | CArray of instance_expr option * constr_expr array * constr_expr * 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
    (*

    argument, measure, relation

    *)
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
and constr_notation_substitution = constr_expr list * constr_expr list list * kinded_cases_pattern_expr list * local_binder_expr list list
type constr_pattern_expr = constr_expr

Concrete syntax for modules and module types

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 * Libnames.qualid
  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