package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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