package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

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/module-type-ExtS/index.html

Module type `Grammar.ExtS`Source

type keyword_state

module EState : sig ... end

module GState : sig ... end

include S
  with type keyword_state := keyword_state
   and type 'a with_gstate := GState.t -> 'a
   and type 'a with_kwstate := keyword_state -> 'a
   and type 'a with_estate := EState.t -> 'a
   and type 'a mod_estate := EState.t -> EState.t * 'a

type te

type 'c pattern

type ty_pattern =

| TPattern : 'a pattern -> ty_pattern

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

module Parsable : sig ... end

module Entry : sig ... end

module Symbol : sig ... end

module Rule : sig ... end

module Rules : sig ... end

module Production : sig ... end

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

type '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.
*)

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

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

type 's add_kw = {

add_kw : 'c. 's -> 'c pattern -> 's;

}

val safe_extend : 
  's add_kw ->
  EState.t ->
  's ->
  'a Entry.t ->
  'a extend_statement ->
  EState.t * 's

module Unsafe : sig ... end