package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
type side =
  1. | Left
  2. | Right
type gram_assoc =
  1. | NonA
  2. | RightA
  3. | LeftA
type gram_position =
  1. | First
  2. | Last
  3. | Before of string
  4. | After of string
  5. | Level of string
type production_position =
  1. | BorderProd of side * gram_assoc option
  2. | InternalProd
type production_level =
  1. | NextLevel
  2. | NumLevel of int
type (!'lev, !'pos) constr_entry_key_gen =
  1. | ETName
  2. | ETReference
  3. | ETBigint
  4. | ETBinder of bool
  5. | ETConstr of 'lev * 'pos
  6. | ETPattern
  7. | ETOther of string * string
  8. | ETConstrList of 'lev * 'pos * Tok.t list
  9. | ETBinderList of bool * Tok.t list
type constr_entry_key = (int, unit) constr_entry_key_gen
type constr_prod_entry_key = (production_level, production_position) constr_entry_key_gen
type simple_constr_prod_entry_key = (production_level, unit) constr_entry_key_gen
type !'a user_symbol =
  1. | Ulist1 of 'a user_symbol
  2. | Ulist1sep of 'a user_symbol * string
  3. | Ulist0 of 'a user_symbol
  4. | Ulist0sep of 'a user_symbol * string
  5. | Uopt of 'a user_symbol
  6. | Uentry of 'a
  7. | Uentryl of 'a * int
type (!'self10, !'a7) symbol =
  1. | Atoken : Tok.t -> ('self, string) symbol
  2. | Alist1 : ('self0, 'a) symbol -> ('self0, 'a list) symbol
  3. | Alist1sep : ('self1, 'a0) symbol * ('self1, 'b) symbol -> ('self1, 'a0 list) symbol
  4. | Alist0 : ('self2, 'a1) symbol -> ('self2, 'a1 list) symbol
  5. | Alist0sep : ('self3, 'a2) symbol * ('self3, 'c) symbol -> ('self3, 'a2 list) symbol
  6. | Aopt : ('self4, 'a3) symbol -> ('self4, 'a3 option) symbol
  7. | Aself : ('self5, 'self5) symbol
  8. | Anext : ('self6, 'self6) symbol
  9. | Aentry : 'a4 entry -> ('self7, 'a4) symbol
  10. | Aentryl : 'a5 entry * int -> ('self8, 'a5) symbol
  11. | Arules : 'a6 rules list -> ('self9, 'a6) symbol
and (!'self1, !_, !'r1) rule =
  1. | Stop : ('self, 'r, 'r) rule
  2. | Next : ('self0, 'a, 'r0) rule * ('self0, 'b) symbol -> ('self0, 'b -> 'a, 'r0) rule
and (!'a, !'r) norec_rule = {
  1. norec_rule : 's. ('s, 'a, 'r) rule;
}
and !'a0 rules =
  1. | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
type !'a0 production_rule =
  1. | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
type !'a single_extend_statment = string option * gram_assoc option * 'a production_rule list
type !'a extend_statment = gram_position option * 'a single_extend_statment 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