package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.interp/Notation_term/index.html
Module Notation_termSource
notation_constr
notation_constr is the subtype of glob_constr allowed in syntactic extensions (i.e. notations). No location since intended to be substituted at any place of a text. Complex expressions such as fixpoints and cofixpoints are excluded, as well as non global expressions such as existential variables.
type notation_constr = | NRef of Names.GlobRef.t * Glob_term.glob_level list option| NVar of Names.Id.t| NApp of notation_constr * notation_constr list| NProj of Names.Constant.t * Glob_term.glob_level list option * notation_constr list * notation_constr| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option| NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool| NLambda of Names.Name.t * notation_constr option * notation_constr| NProd of Names.Name.t * notation_constr option * notation_constr| NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool| NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr| NCases of Constr.case_style * notation_constr option * (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list * (Glob_term.cases_pattern list * notation_constr) list| NLetTuple of Names.Name.t list * Names.Name.t * notation_constr option * notation_constr * notation_constr| NIf of notation_constr * Names.Name.t * notation_constr option * notation_constr * notation_constr| NRec of Glob_term.glob_fix_kind * Names.Id.t array * (Names.Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array| NSort of Glob_term.glob_sort| NCast of notation_constr * Constr.cast_kind * notation_constr| NInt of Uint63.t| NFloat of Float64.t| NArray of notation_constr array * notation_constr * notation_constr
Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted in iterator and snd id is alternative name just for printing; boolean is associativity
Types concerning notations
Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y
type notation_binder_source = | NtnParsedAsPattern of bool| NtnParsedAsIdent| NtnParsedAsName| NtnBinderParsedAsConstr of constr_as_binder_kind| NtnParsedAsBinder
type notation_var_instance_type = | NtnTypeConstr| NtnTypeBinder of notation_binder_source| NtnTypeConstrList| NtnTypeBinderList
type notation_var_internalization_type = | NtnInternTypeAny of scope_name option| NtnInternTypeOnlyBinder
Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y
type interpretation =
(Names.Id.t * (extended_subscopes * notation_var_instance_type)) list
* notation_constrThis characterizes to what a notation is interpreted to
type notation_interp_env = {ninterp_var_type : notation_var_internalization_type Names.Id.Map.t;ninterp_rec_vars : Names.Id.t Names.Id.Map.t;
}type interp_rule = | NotationRule of Constrexpr.specific_notation| AbbrevRule of Names.KerName.t