package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Entry keys for constr notations

type side =
  1. | Left
  2. | Right
type production_position =
  1. | BorderProd of side * Gramlib.Gramext.g_assoc option
  2. | InternalProd
type production_level =
  1. | NextLevel
  2. | NumLevel of int
  3. | DefaultLevel
    (*

    Interpreted differently at the border or inside a rule

    *)
val production_level_eq : production_level -> production_level -> bool

User-level types used to tell how to parse or interpret of the non-terminal

type 'a constr_entry_key_gen =
  1. | ETIdent
  2. | ETName of bool
  3. | ETGlobal
  4. | ETBigint
  5. | ETBinder of bool
  6. | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
  7. | ETPattern of bool * int option

Entries level (left-hand side of grammar rules)

type constr_entry_key = (production_level * production_position) constr_entry_key_gen
val constr_entry_key_eq : constr_entry_key -> constr_entry_key -> bool

Entries used in productions, vernac side (e.g. "x bigint" or "x ident")

type simple_constr_prod_entry_key = production_level constr_entry_key_gen

Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals

type binder_entry_kind =
  1. | ETBinderOpen
  2. | ETBinderClosed of (bool * string) list
type binder_target =
  1. | ForBinder
  2. | ForTerm
type constr_prod_entry_key =
  1. | ETProdIdent
  2. | ETProdName
  3. | ETProdReference
  4. | ETProdBigint
  5. | ETProdOneBinder of bool
  6. | ETProdConstr of Constrexpr.notation_entry * production_level * production_position
  7. | ETProdPattern of int
  8. | ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * (bool * string) list
  9. | ETProdBinderList of binder_entry_kind
AST for user-provided entries
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 ('a, 'b, 'c) ty_user_symbol =
  1. | TUlist1 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
  2. | TUlist1sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
  3. | TUlist0 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
  4. | TUlist0sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
  5. | TUopt : ('a, 'b, 'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
  6. | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a, 'b, 'c) ty_user_symbol
  7. | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a, 'b, 'c) ty_user_symbol
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