package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ConstrexprSource

Concrete syntax for terms
Sourcetype 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

Sourcetype sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
Sourcetype instance_expr = univ_level_expr list

Constraints don't have anonymous universes

Sourcetype cumul_univ_decl_expr = ((Names.lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
Sourcetype ident_decl = Names.lident * universe_decl_expr option
Sourcetype cumul_ident_decl = Names.lident * cumul_univ_decl_expr option
Sourcetype name_decl = Names.lname * universe_decl_expr option
Sourcetype notation_with_optional_scope =
  1. | LastLonelyNotation
  2. | NotationInScope of string
Sourcetype entry_level = int
Sourcetype entry_relative_level =
  1. | LevelLt of entry_level
  2. | LevelLe of entry_level
  3. | LevelSome
Sourcetype notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
Sourcetype notation_entry_level =
  1. | InConstrEntrySomeLevel
  2. | InCustomEntryLevel of string * entry_level
Sourcetype notation_key = string
Sourcetype 'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
Sourcetype 'a or_by_notation = 'a or_by_notation_r CAst.t
Sourcetype explicitation =
  1. | ExplByPos of int * Names.Id.t option
  2. | ExplByName of Names.Id.t
Sourcetype 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

    *)
Sourcetype abstraction_kind =
  1. | AbsLambda
  2. | AbsPi
Sourcetype proj_flag = int option

Some n = proj of the n-th visible argument

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

Sourceand cases_pattern_expr = cases_pattern_expr_r CAst.t
Sourceand kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
Sourceand cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list
Sourceand 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 CAst.t * (Names.lident * constr_expr) list
  16. | CSort of sort_expr
  17. | CCast of constr_expr * constr_expr Glob_term.cast_type
  18. | CNotation of notation_with_optional_scope option * 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
  22. | CArray of instance_expr option * constr_expr array * constr_expr * constr_expr
Sourceand constr_expr = constr_expr_r CAst.t
Sourceand case_expr = constr_expr * Names.lname option * cases_pattern_expr option
Sourceand branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t
Sourceand 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

    *)
Sourceand recursion_order_expr = recursion_order_expr_r CAst.t
Sourceand 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
Sourceand constr_notation_substitution = constr_expr list * constr_expr list list * kinded_cases_pattern_expr list * local_binder_expr list list
Sourcetype constr_pattern_expr = constr_expr

Concrete syntax for modules and module types

Sourcetype 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
Sourcetype module_ast_r =
  1. | CMident of Libnames.qualid
  2. | CMapply of module_ast * module_ast
  3. | CMwith of module_ast * with_declaration_ast
Sourceand 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