Coq: Notations


Info

From camlp5 docs:

A grammar entry is an abstract value internally containing a stream parser

Print Grammar constructor.
(*
Entry constructor is
[ LEFTA
  [ quoted_attributes; identref; constructor_type ] ]
*)

Entries:

Also see:

Syntax modifiers

https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#grammar-token-syntax_modifier

local attribute

If local attribute is used, notation is available only within the same module.

Module FooMod.
  #[local] Notation "⊥" := false.

  Check ⊥.  (* ⊥ : bool *)
End FooMod.

Import FooMod.
Compute ⊥.
(* Syntax Error: Lexer: Undefined token *)

Reserved Notation

Same notations may have different meaning in different contexts. But they must all have the same precedence and associativity.

We can 'reserve' notations to ensure that.

Reserved Infix is the same thing except that the notation is infix.

Syntax modifier

Other:

Custom entries

constr: the predefined grammar entry. As in the default interpretation.

We can make our own grammar entries via Custom Entry.

Precedence

Lower the precedence level, higher the precedence.

Examples

Documentation mentions this example of having left-associative tuples:

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).

Set Printing Parentheses.
Check (1,2,3).
(* ((1, 2), 3) : (nat * nat) * nat *)

We can have a right-associative version like:

Notation "( x , .. , y , z )" := (pair x .. (pair y z) .. ) (at level 0).

Set Printing Parentheses.
Check (1,2,3).
(* (1, (2, 3)) : nat * (nat * nat) *)

Thanks to https://coq.zulipchat.com/#narrow/stream/423352-Coq-Notation-system

Todo