package coq

  1. Overview
  2. Docs
package coq
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.

type notation_constr =
  1. | NRef of Names.GlobRef.t * Glob_term.glob_level list option
  2. | NVar of Names.Id.t
  3. | NApp of notation_constr * notation_constr list
  4. | NProj of Names.Constant.t * Glob_term.glob_level list option * notation_constr list * notation_constr
  5. | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
  6. | NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
  7. | NLambda of Names.Name.t * notation_constr option * notation_constr
  8. | NProd of Names.Name.t * notation_constr option * notation_constr
  9. | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
  10. | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr
  11. | 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
  12. | NLetTuple of Names.Name.t list * Names.Name.t * notation_constr option * notation_constr * notation_constr
  13. | NIf of notation_constr * Names.Name.t * notation_constr option * notation_constr * notation_constr
  14. | 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
  15. | NSort of Glob_term.glob_sort
  16. | NCast of notation_constr * Constr.cast_kind * notation_constr
  17. | NInt of Uint63.t
  18. | NFloat of Float64.t
  19. | 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 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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct