package coq-core

  1. Overview
  2. Docs
package coq-core
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
  6. | NGenarg of Genarg.glob_generic_argument
  7. | NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
  8. | NLambda of Names.Name.t * notation_constr option * notation_constr
  9. | NProd of Names.Name.t * notation_constr option * notation_constr
  10. | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
  11. | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr
  12. | 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
  13. | NLetTuple of Names.Name.t list * Names.Name.t * notation_constr option * notation_constr * notation_constr
  14. | NIf of notation_constr * Names.Name.t * notation_constr option * notation_constr * notation_constr
  15. | 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
  16. | NSort of Glob_term.glob_sort
  17. | NCast of notation_constr * Constr.cast_kind option * notation_constr
  18. | NInt of Uint63.t
  19. | NFloat of Float64.t
  20. | 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 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 =
  1. | AsIdent
  2. | AsName
  3. | AsAnyPattern
  4. | AsStrictPattern
type notation_binder_source =
  1. | NtnBinderParsedAsConstr of notation_binder_kind
  2. | NtnBinderParsedAsSomeBinderKind of notation_binder_kind
  3. | NtnBinderParsedAsBinder
type notation_var_instance_type =
  1. | NtnTypeConstr
  2. | NtnTypeConstrList
  3. | NtnTypeBinder of notation_binder_source
  4. | NtnTypeBinderList of notation_binder_source
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