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_var_instance_type =
  1. | NtnTypeConstr
  2. | NtnTypeOnlyBinder
  3. | NtnTypeConstrList
  4. | NtnTypeBinderList
type notation_var_internalization_type =
  1. | NtnInternTypeConstr
  2. | NtnInternTypeBinder
  3. | NtnInternTypeIdent
type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * notation_constr
type reversibility_flag = bool
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
type one_notation_grammar = {
  1. notgram_level : int;
  2. notgram_assoc : Extend.gram_assoc option;
  3. notgram_notation : Constrexpr.notation;
  4. notgram_prods : grammar_constr_prod_item list list;
  5. notgram_typs : notation_var_internalization_type list;
}
type notation_grammar = bool * 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