Module Constrexpr
Concrete syntax for terms
type universe_decl_expr
= (Names.lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
constr_expr
is the abstract syntax tree produced by the parser
type ident_decl
= Names.lident * universe_decl_expr option
type name_decl
= Names.lname * universe_decl_expr option
type notation_entry
=
|
InConstrEntry
|
InCustomEntry of string
type notation_entry_level
=
|
InConstrEntrySomeLevel
|
InCustomEntryLevel of string * int
type notation_key
= string
type notation
= notation_entry_level * notation_key
type 'a or_by_notation_r
=
|
AN of 'a
|
ByNotation of string * string option
type 'a or_by_notation
= 'a or_by_notation_r CAst.t
type explicitation
=
|
ExplByPos of int * Names.Id.t option
|
ExplByName of Names.Id.t
type binder_kind
=
|
Default of Decl_kinds.binding_kind
|
Generalized of Decl_kinds.binding_kind * bool
(Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses
type abstraction_kind
=
|
AbsLambda
|
AbsPi
type proj_flag
= int option
Some n
= proj of the n-th visible argument
type sign
=
|
SPlus
|
SMinus
type raw_numeral
= NumTok.t
type prim_token
=
|
Numeral of sign * raw_numeral
|
String of string
type instance_expr
= Glob_term.glob_level list
type cases_pattern_expr_r
=
|
CPatAlias of cases_pattern_expr * Names.lname
|
CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list
CPatCstr (_, c, Some l1, l2)
represents(@ c l1) l2
|
CPatAtom of Libnames.qualid option
|
CPatOr of cases_pattern_expr list
|
CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list
CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2
|
CPatPrim of prim_token
|
CPatRecord of (Libnames.qualid * cases_pattern_expr) list
|
CPatDelimiters of string * cases_pattern_expr
|
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
=
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 fix_expr
= Names.lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr
and cofix_expr
= Names.lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr_r
=
|
CStructRec of Names.lident
|
CWfRec of Names.lident * constr_expr
|
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
=
|
CLocalAssum of Names.lname list * binder_kind * constr_expr
|
CLocalDef of Names.lname * constr_expr * constr_expr option
|
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
=
|
CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
|
CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r
=
|
CMident of Libnames.qualid
|
CMapply of module_ast * module_ast
|
CMwith of module_ast * with_declaration_ast
and module_ast
= module_ast_r CAst.t