CoqWG Activity

Print Notation Command

Discussion for issue https://github.com/coq/coq/issues/14907 Draft PR: https://github.com/coq/coq/pull/15683

participants: Ana, Rodrigo, Ali, Emilio

• SerAPI has a similar command, we had a look, just a wrapper over existing Coq APIs.
• Difference between the notation information, and the parser grammar (once the notation has been added)
• Notations in Coq are just strings, i.e. "_ + _". See Notgram_ops.get_defined_notations
• Implementation to happen in two phases:
  • First phase: register a new vernac command
  • Second phase: implement the command's functionality

To register a new vernac command:

1. update vernac/vernacexpr.ml to add an ast for Print Notation
2. update vernac/g_vernac.mlg to add a parsing rule (similar to other Print stuff, grep for PrintCoercions)
3. hook in vernac/vernacentries the implementation:

The implementation has to:

1. resolve user input (here you may want to split Notation.locate_notation)
2. query Coq for notation data (Notgram_ops.grammar_of_notation)
3. display notation data (up to what we consider pleasant)

Additional concerns:

• what to when there are many candidates (as in Locate "+".)
• Separation of concerns between logic and display

Log

• Tuesday 15/02/2022
  • The vernac command has been added.
  • A PR has been submitted: https://github.com/coq/coq/pull/15683
• Wednesday 16/02/2022
  • The vernac command now prints information about the level and the associativity.
• Thursday 17/02/2022
  • An error message is now produced when the notation can not be found.

Coq Internals

[Emilio will fill some details and pointers]