package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.printing/Ppextend/index.html

Module `Ppextend`Source

Pretty-print.

Sourcetype ppbox =

| PpHB
| PpHOVB of int
| PpHVB of int
| PpVB of int

Sourcetype ppcut =

| PpBrk of int * int
| PpFnl

Sourceval ppcmd_of_box : ppbox -> Pp.t -> Pp.t

Sourceval ppcmd_of_cut : ppcut -> Pp.t

Printing rules for notations

Sourcetype pattern_quote_style =

| QuotedPattern
| NotQuotedPattern

Sourcetype unparsing =

| UnpMetaVar of Constrexpr.notation_entry_relative_level
| UnpBinderMetaVar of Constrexpr.notation_entry_relative_level * pattern_quote_style
| UnpListMetaVar of Constrexpr.notation_entry_relative_level * unparsing list
| UnpBinderListMetaVar of bool * bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut

Declare and look for the printing rule for symbolic notations

Sourcetype unparsing_rule = unparsing list

Sourceval unparsing_eq : unparsing -> unparsing -> bool

Sourcetype notation_printing_rules = {

notation_printing_unparsing : unparsing_rule;
notation_printing_level : Constrexpr.entry_level;

}

Sourcetype generic_notation_printing_rules = {

notation_printing_reserved : bool;
notation_printing_rules : notation_printing_rules;

}

Source

val declare_generic_notation_printing_rules : 
  Constrexpr.notation ->
  generic_notation_printing_rules ->
  unit

Source

val declare_specific_notation_printing_rules : 
  Constrexpr.specific_notation ->
  notation_printing_rules ->
  unit

Sourceval has_generic_notation_printing_rule : Constrexpr.notation -> bool

Source

val find_generic_notation_printing_rule : 
  Constrexpr.notation ->
  generic_notation_printing_rules

Source

val find_specific_notation_printing_rule : 
  Constrexpr.specific_notation ->
  notation_printing_rules

Source

val find_notation_printing_rule : 
  Constrexpr.notation_with_optional_scope option ->
  Constrexpr.notation ->
  notation_printing_rules

On This Page

Pretty-print.
Printing rules for notations

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.printing/Ppextend/index.html

Module PpextendSource

Pretty-print.

Printing rules for notations

Module `Ppextend`Source