Notation_termnotation_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. Non global expressions such as existential variables are not allowed.
type notation_constr = | NRef of Names.GlobRef.t * Glob_term.glob_instance option| NVar of Names.Id.t| NApp of notation_constr * notation_constr list| NProj of Names.Constant.t * Glob_term.glob_instance option
* notation_constr list
* notation_constr| NHole of Glob_term.glob_evar_kind| NGenarg of GenConstr.glb| 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 option * notation_constr| NInt of Uint63.t| NFloat of Float64.t| NString of Pstring.t| NArray of notation_constr array * notation_constr * notation_constrNote 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 tmp_scope_name = scope_nametype subscopes = Constrexpr.scope_delimiter listtype extended_subscopes = Constrexpr.notation_entry_relative_level * subscopestype notation_var_binders = Names.Id.Set.tThe set of other notation variables that are bound to a binder or binder list and that bind the given notation variable, for instance, in "{ x | P }" := (sigT (fun x => P), "x" is under an empty set of binders and "P" is under the binders bound to "x", that is, its notation_var_binders set is "x"
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 = | NtnBinderParsedAsConstr of notation_binder_kind| NtnBinderParsedAsSomeBinderKind of notation_binder_kind| NtnBinderParsedAsBindertype notation_var_kind = | NtnTypeVarConstr of notation_var_constr_kind| NtnTypeVarPattern of notation_binder_source| NtnTypeVarBinders of notation_binder_sourceType of variables in notation interpretations, remembering how it is parsed; Note: when a notation variable appears both as term and as binder, its type is Pattern
type notation_var_type = | NtnTypeVar of extended_subscopes * notation_var_binders * notation_var_kind| NtnTypeVarList of notation_var_type| NtnTypeVarTuple of notation_var_type listtype notation_var_internalization_type = | NtnInternTypeAny of scope_name option| NtnInternTypeOnlyBinderType 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 'a interpretation_gen = (Names.Id.t * 'a) list * notation_constrThis characterizes to what a notation is interpreted to
type interpretation = notation_var_type interpretation_gentype reversibility_status = | APrioriReversible| Forgetful of forgetfulness| NonInjective of Names.Id.t listtype notation_interp_var_types =
notation_var_internalization_type Names.Id.Map.ttype 'a notation_raw_type = | NtnRawTypeVar of 'a| NtnRawTypeVarList of ('a * 'a) notation_raw_type| NtnRawTypeVarTuple of 'a notation_raw_type listtype notation_interp_env = {ninterp_var_type : notation_interp_var_types;ninterp_raw_types : Names.Id.t notation_raw_type list;}