package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

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

Module Grammar.GMakeSource

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
Sourcetype 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list
Sourcetype 'a extend_statement =
  1. | Reuse of string option * 'a Production.t list
    (*

    Extend an existing level by its optional given name. If None, picks the topmost level.

    *)
  2. | Fresh of Gramext.position * 'a single_extend_statement list
    (*

    Create a level at the given position.

    *)
Sourceval 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