package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module L : Plexing.S

Signature

module EState : sig ... end
module 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
type 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 Pcoq

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 =
  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.

    *)
val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
type 's add_kw = {
  1. add_kw : 'c. 's -> 'c L.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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct