package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz

md5=8d852367b54f095d9fbabd000304d450

sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

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

Module `Grammar.GMake`Source

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 =

| TPattern : 'a L.pattern -> ty_pattern

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

Sourcemodule Parsable : sig ... end

Sourcemodule Entry : sig ... end

Sourcemodule Symbol : sig ... end

Sourcemodule Rule : sig ... end

Sourcemodule Rules : sig ... end

Sourcemodule Production : sig ... end

Source

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

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

Source

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

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

Sourcetype 's add_kw = {

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

}

Source

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

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

Sourcemodule Unsafe : sig ... end

On This Page

Parameters
Signature

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Grammar.GMakeSource

Parameters

Signature

Module `Grammar.GMake`Source