_ /\ _
, _ || _
Print Notation "_ :: _"
: Show info of a notation, including its level and associativityPrint Grammar
constr
From camlp5 docs:
A grammar entry is an abstract value internally containing a stream parser
—
Print Grammar constr.
: Print grammar for the entry named constr
Print Grammar.
: Print whole gramamrPrint Custom Grammar <custom-entry-name>
: print grammar of a custom entryPrint Grammar constructor.
(*
Entry constructor is
[ LEFTA
[ quoted_attributes; identref; constructor_type ] ]
*)
Entries:
constr
: termsvernac
: vernacular commandstactic
: tacticsltac2
: ltac2 stuff, I guessAlso see:
local
attributeIf 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.
x name
: 'parse x
as a single identifier'x at level 10
: x is parsed as a term at level 10, but is actually to be a nameOther:
p pattern
: p is a pattern. Like the kind used in pattern matching.constr
: the predefined grammar entry. As in the default interpretation.
We can make our own grammar entries via Custom Entry
.
Print Custom Grammar <custom-entry-name>
constr
: Print Grammar constr
Lower the precedence level, higher the precedence.
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