package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.gramlib/Gramlib/Grammar/GMake/index.html

Module Grammar.GMakeSource

Parameters

module L : Plexing.S

Signature

Sourcemodule EState : sig ... end
Sourcemodule GState : sig ... end
include S with type keyword_state := L.keyword_state and type 'a with_gstate := GState.t -> 'a and type 'a with_kwstate := L.keyword_state -> 'a and type 'a with_estate := EState.t -> 'a and type 'a mod_estate := EState.t -> EState.t * 'a with type te := L.te with type 'c pattern := 'c L.pattern
Sourcetype ty_pattern =
  1. | TPattern : 'a L.pattern -> ty_pattern

Type combinators to factor the module type between explicit state passing in Grammar and global state in Procq

Sourcemodule Parsable : sig ... end
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 -> ('b, norec, 'c) Symbol.t option
Sourceval level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
Sourcetype 's add_kw = {
  1. add_kw : 'c. 's -> 'c L.pattern -> 's;
}
Sourceval safe_extend : 's add_kw -> EState.t -> 's -> 'a Entry.t -> 'a extend_statement -> EState.t * 's
Sourcemodule Unsafe : sig ... end