Module 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.

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 scope_name = string
type tmp_scope_name = scope_name
type subscopes = tmp_scope_name list * scope_name list

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_kind =
| AsIdent
| AsName
| AsAnyPattern
| AsStrictPattern
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"

This characterizes to what a notation is interpreted to

type forgetfulness = {
forget_ltac : bool;
forget_volatile_cast : bool;
}
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;
}