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.17.0.tar.gz

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

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

Source

type 'te lexer_func =
  ?loc:Loc.t ->
  ?fix_loc:(Loc.t -> Loc.t) ->
  char Stream.t ->
  'te LStream.t

Returning a stream equipped with a location function

Sourcemodule type S = sig ... end