Notation_term
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 =
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 tmp_scope_name = scope_name
type subscopes = tmp_scope_name list * scope_name list
type extended_subscopes = Constrexpr.notation_entry_relative_level * subscopes
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 |
| NtnBinderParsedAsBinder |
type notation_var_instance_type =
| NtnTypeConstr |
| NtnTypeConstrList |
| NtnTypeBinder of notation_binder_source |
| NtnTypeBinderList of notation_binder_source |
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 notation_var_binders = Names.Id.Set.t
The 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 interpretation = (Names.Id.t * (extended_subscopes * notation_var_binders * notation_var_instance_type)) list * notation_constr
This characterizes to what a notation is interpreted to
type reversibility_status =
| APrioriReversible |
| Forgetful of forgetfulness |
| NonInjective of Names.Id.t list |
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; |
}