package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.parsing/Extend/index.html
Module ExtendSource
Entry keys for constr notations
Source
type production_position = | BorderProd of Constrexpr.side * Gramlib.Gramext.g_assoc option| InternalProd
User-level types used to tell how to parse or interpret of the non-terminal
Source
type 'a constr_entry_key_gen = | ETIdent| ETName| ETGlobal| ETBigint| ETBinder of bool| ETConstr of Constrexpr.notation_entry * Notation_term.notation_binder_kind option * 'a| ETPattern of bool * int option
Entries level (left-hand side of grammar rules)
Entries used in productions, vernac side (e.g. "x bigint" or "x ident")
Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals
Source
type binder_entry_kind = | ETBinderOpen| ETBinderClosed of constr_prod_entry_key option * (bool * string) list
Source
and constr_prod_entry_key = | ETProdIdent| ETProdName| ETProdGlobal| ETProdBigint| ETProdOneBinder of bool| ETProdConstr of Constrexpr.notation_entry * production_level * production_position| ETProdPattern of int| ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * (bool * string) list| ETProdBinderList of binder_entry_kind
AST for user-provided entries
Source
type 'a user_symbol = | Ulist1 of 'a user_symbol| Ulist1sep of 'a user_symbol * string| Ulist0 of 'a user_symbol| Ulist0sep of 'a user_symbol * string| Uopt of 'a user_symbol| Uentry of 'a| Uentryl of 'a * int
Source
type ('a, 'b, 'c) ty_user_symbol = | TUlist1 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol| TUlist1sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol| TUlist0 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol| TUlist0sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol| TUopt : ('a, 'b, 'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a, 'b, 'c) ty_user_symbol| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a, 'b, 'c) ty_user_symbol
On This Page