package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.gramlib/Gramlib/Grammar/index.html
Module Gramlib.Grammar
Source
Extensible grammars.
This module implements the Camlp5 extensible grammars system. Grammars entries can be extended using the EXTEND
statement, added by loading the Camlp5 pa_extend.cmo
file.
Raised by parsers when the first component of a stream pattern is accepted, but one of the following components is rejected.
Functorial interface
Alternative for grammars use. Grammars are no more Ocaml values: there is no type for them. Modules generated preserve the rule "an entry cannot call an entry of another grammar" by normal OCaml typing.
The input signature for the functor Grammar.GMake
: te
is the type of the tokens.
Signature type of the functor Grammar.GMake
. The types and functions are almost the same than in generic interface, but:
- Grammars are not values. Functions holding a grammar as parameter do not have this parameter yet.
- The type
parsable
is used in functionparse
instead of the char stream, avoiding the possible loss of tokens. - The type of tokens (expressions and patterns) can be any type (instead of (string * string)); the module parameter must specify a way to show them as (string * string)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page