package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type scope_name = string
type tmp_scope_name = scope_name
type subscopes = tmp_scope_name option * scope_name list
type notation_binder_source =
  1. | NtnParsedAsPattern of bool
  2. | NtnParsedAsIdent
  3. | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
type notation_var_instance_type =
  1. | NtnTypeConstr
  2. | NtnTypeBinder of notation_binder_source
  3. | NtnTypeConstrList
  4. | NtnTypeBinderList
type notation_var_internalization_type =
  1. | NtnInternTypeAny
  2. | NtnInternTypeOnlyBinder
type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * notation_constr
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;
}
type grammar_constr_prod_item =
  1. | GramConstrTerminal of Tok.t
  2. | GramConstrNonTerminal of Extend.constr_prod_entry_key * Names.Id.t option
  3. | GramConstrListMark of int * bool * int
type precedence = int
type parenRelation =
  1. | L
  2. | E
  3. | Any
  4. | Prec of precedence
type tolerability = precedence * parenRelation
type one_notation_grammar = {
  1. notgram_level : level;
  2. notgram_assoc : Extend.gram_assoc option;
  3. notgram_notation : Constrexpr.notation;
  4. notgram_prods : grammar_constr_prod_item list list;
}
type notation_grammar = {
  1. notgram_onlyprinting : bool;
  2. notgram_rules : one_notation_grammar list;
}
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