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

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.gramlib/Gramlib/Grammar/GMake/index.html

Module `Grammar.GMake`Source

Parameters

module L : Plexing.S

Signature

include S with type te = L.te with type 'c pattern = 'c L.pattern

Sourcetype te = L.te

Sourcetype 'c pattern = 'c L.pattern

Sourcemodule Parsable : sig ... end

Sourceval tokens : string -> (string option * int) list

Sourcemodule Entry : sig ... end

Sourcemodule Symbol : sig ... end

Sourcemodule Rule : sig ... end

Sourcemodule Rules : sig ... end

Sourcemodule Production : sig ... end

Source

type 'a single_extend_statement =
  string option * Gramext.g_assoc option * 'a Production.t list

Sourcetype 'a extend_statement =

| Reuse of string option * 'a Production.t list
(*
Extend an existing level by its optional given name. If None, picks the topmost level.
*)
| Fresh of Gramext.position * 'a single_extend_statement list
(*
Create a level at the given position.
*)

Source

val generalize_symbol : 
  ('a, 'tr, 'c) Symbol.t ->
  ('a, norec, 'c) Symbol.t option

Sourceval mk_rule : 'a pattern list -> string Rules.t

Sourceval level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option

Sourceval safe_extend : 'a Entry.t -> 'a extend_statement -> unit

Sourceval safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit

Sourcemodule Unsafe : sig ... end

On This Page

Parameters
Signature