package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.vernac/Metasyntax/index.html

Module MetasyntaxSource

Sourcetype notation_main_data
Sourcetype syntax_rules
Sourcetype 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.

Sourceval 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

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

Declare the interpretation of a notation

Declaring scopes, delimiter keys and default scopes

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

Scope opening

Sourceval 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

Sourceval 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

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

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

Print the Camlp5 state of a grammar

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

Declare given string as a custom grammar entry

Sourceval 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