package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 option * scope_name list
type extended_subscopes = Constrexpr.notation_entry_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 constr_as_binder_kind =
  1. | AsIdent
  2. | AsName
  3. | AsNameOrPattern
  4. | AsStrictPattern
type notation_binder_source =
  1. | NtnParsedAsPattern of bool
  2. | NtnParsedAsIdent
  3. | NtnParsedAsName
  4. | NtnBinderParsedAsConstr of constr_as_binder_kind
  5. | NtnParsedAsBinder
type notation_var_instance_type =
  1. | NtnTypeConstr
  2. | NtnTypeBinder of notation_binder_source
  3. | NtnTypeConstrList
  4. | NtnTypeBinderList
type notation_var_internalization_type =
  1. | NtnInternTypeAny of scope_name option
  2. | 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

This characterizes to what a notation is interpreted to

type reversibility_status =
  1. | APrioriReversible
  2. | HasLtac
  3. | NonInjective of Names.Id.t list
type notation_interp_env = {
  1. ninterp_var_type : notation_var_internalization_type Names.Id.Map.t;
  2. ninterp_rec_vars : Names.Id.t Names.Id.Map.t;
}
OCaml

Innovation. Community. Security.