package coq-core

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

This data type packages all the necessary information to declare a notation interpretation, once the syntax is declared or recovered from a previous declaration.

val add_notation_syntax : local:bool -> infix:bool -> UserWarn.t option -> Vernacexpr.notation_declaration -> notation_interpretation_decl

Add syntax rules for a (constr) notation in the environment

val add_notation_interpretation : local:bool -> Environ.env -> notation_interpretation_decl -> unit

Declare the interpretation of a notation

Declaring scopes, delimiter keys and default scopes

val declare_scope : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit
val add_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> string -> unit
val remove_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit

Scope opening

val open_close_scope : Vernacexpr.locality_flag -> to_open:bool -> Notation_term.scope_name -> unit

Add a notation interpretation associated to a "where" clause (already has pa/pp rules)

Interpret the modifiers of a where-notation

val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> notation_interpretation_decl -> unit

Set the interpretation of the where-notation for interpreting a mutual block

Add only the parsing/printing rule of a notation

val add_reserved_notation : local:bool -> infix:bool -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t list) -> unit

Add a syntactic definition (as in "Notation f := ...")

val add_abbreviation : local:bool -> UserWarn.t option -> Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> Vernacexpr.syntax_modifier CAst.t list -> unit

Print the Camlp5 state of a grammar

val pr_grammar : string list -> Pp.t
val pr_custom_grammar : string -> Pp.t
val pr_keywords : unit -> Pp.t
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_notation_toggle : Vernacexpr.locality_flag -> on:bool -> all:bool -> Notation.notation_query_pattern -> unit
val declare_custom_entry : Vernacexpr.locality_flag -> string -> unit

Declare given string as a custom grammar entry

val check_custom_entry : string -> unit

Check that the given string is a valid custom entry that has been declared

Pretty print level information of a notation and all of its arguments

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