package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.1.tar.gz

sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.gramlib/Gramlib/Plexing/index.html

Module `Gramlib.Plexing`Source

Lexing for Camlp5 grammars.

This module defines the Camlp5 lexer type to be used in extensible grammars (see module Grammar). It also provides some useful functions to create lexers.

Lexer type

Sourcetype 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te LStream.t

Returning a stream equipped with a location function

Sourcemodule type S = sig ... end