package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.parsing/Extend/index.html
Module ExtendSource
Entry keys for constr notations
Source
type production_position = | BorderProd of 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.constr_as_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 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