package coq-core

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

The type of token for the Coq lexer and parser

type 'c p =
  1. | PKEYWORD : string -> string p
  2. | PPATTERNIDENT : string option -> string p
  3. | PIDENT : string option -> string p
  4. | PFIELD : string option -> string p
  5. | PNUMBER : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
  6. | PSTRING : string option -> string p
  7. | PLEFTQMARK : unit p
  8. | PBULLET : string option -> string p
  9. | PQUOTATION : string -> string p
  10. | PEOI : unit p
val pattern_strings : 'c p -> string * string option
type t =
  1. | KEYWORD of string
  2. | PATTERNIDENT of string
  3. | IDENT of string
  4. | FIELD of string
  5. | NUMBER of NumTok.Unsigned.t
  6. | STRING of string
  7. | LEFTQMARK
  8. | BULLET of string
  9. | QUOTATION of string * string
  10. | EOI
val equal_p : 'a p -> 'b p -> ('a, 'b) Util.eq option
val equal : t -> t -> bool
val extract_string : bool -> t -> string

Names of tokens, used in Grammar error messages

val token_text : 'c p -> string
val trim_quotation : string -> char option * string

Utility function for the test returned by a QUOTATION token: It returns the delimiter parenthesis, if any, and the text without delimiters. Eg `{{ text

}

}

` -> Some '{', ` text `

val match_pattern : 'c p -> t -> 'c

for camlp5, eg GRAMMAR EXTEND ..... [ IDENT "x" -> .... ] END is a pattern (PIDENT (Some "x"))

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