package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.interp/Notation_term/index.html

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.

type notation_constr =
  1. | NRef of Names.GlobRef.t * Glob_term.glob_instance option
  2. | NVar of Names.Id.t
  3. | NApp of notation_constr * notation_constr list
  4. | NProj of Names.Constant.t * Glob_term.glob_instance option * notation_constr list * notation_constr
  5. | NHole of Glob_term.glob_evar_kind
  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. | NString of Pstring.t
  21. | 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

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 = {
  1. forget_ltac : bool;
  2. forget_volatile_cast : bool;
}
type reversibility_status =
  1. | APrioriReversible
  2. | Forgetful of forgetfulness
  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;
}