package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz

md5=8d852367b54f095d9fbabd000304d450

sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

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.

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.

Sourcetype norec

Sourcetype mayrec

Sourcemodule type S = sig ... end

Sourcemodule type ExtS = sig ... end

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 function parse 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)

Source

module GMake
  (L : Plexing.S) : 
  ExtS
    with type keyword_state := L.keyword_state
     and type te := L.te
     and type 'c pattern := 'c L.pattern

On This Page

Functorial interface