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 <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

val safe_delete_rule : EState.t -> 'a Entry.t -> 'a Production.t -> EState.t

module Unsafe : sig ... end