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.gramlib/Gramlib/Grammar/GMake/index.html
Module Grammar.GMake
Source
Parameters
Signature
include S
with type keyword_state := L.keyword_state
and type 'a with_gstate := GState.t -> 'a
and type 'a with_kwstate := L.keyword_state -> 'a
and type 'a with_estate := EState.t -> 'a
and type 'a mod_estate := EState.t -> EState.t * 'a
with type te := L.te
with type 'c pattern := 'c L.pattern
Type combinators to factor the module type between explicit state passing in Grammar and global state in Pcoq
Source
type 'a single_extend_statement =
string option * Gramext.g_assoc option * 'a Production.t list
Source
type 'a extend_statement =
| Reuse of string option * 'a Production.t list
(*Extend an existing level by its optional given name. If None, picks the topmost level.
*)| Fresh of Gramext.position * 'a single_extend_statement list
(*Create a level at the given position.
*)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page