1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(* Various meaningless notations *)
Fail Notation "#" := 0 (only parsing, only parsing).
Fail Notation "#" := 0 (only parsing, only printing).
Fail Notation "#" := 0 (only printing, only printing).
Notation "#" := 0 (only parsing, format "#").
(* Alerting about primitive syntax *)
Notation "1" := tt (at level 3).
Check 1%nat.
Fail Reserved Notation "1".
Notation """tt""" := tt (at level 2).
Check "tt".
Require Import String.
Check "tt"%string.
Fail Reserved Notation """tt""".
(* Test string literals themselves with double quotes *)
Notation """t""""t""" := tt.
Check "t""t".
Module A.
(* Not forced to be a keyword *)
Notation "# ""|"" a" := (Some a) (at level 0, a at level 0).
Check # "|" true.
Check "|"%string.
(* Now forced to be a keyword *)
Notation "a ""|"" b" := (a, b) (at level 50).
Check 2 "|" 4.
End A.
Module B.
Notation " ""I'm true"" " := true.
Check "I'm true".
Notation """""" := false. (* Empty string *)
Check "".
End B.
Module C.
Notation "symbolwith""doublequote" := true (only printing).
Check true.
Notation "'""'" := false (only printing). (* double quote *)
Check false.
End C.
|
