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
54
55
56
57
58
59
60
61
62
63
64
65
66
|
Set Printing All. Set Warnings "-prefix-incompatible-level".
(* if ``~`` and ``~~`` are both defined as tokens,
the inputs ``~ ~`` and ``~~`` generate different tokens *)
Section TestLexer0.
Local Notation "~" := not.
Local Notation "~~" := not.
Check ~ ~ True.
Check ~~ True.
End TestLexer0.
(* whereas if ``~~`` is not defined,
then the two inputs are equivalent *)
Section TestLexer1.
Local Notation "~" := not.
Set Printing All.
Check ~ ~ True.
Check ~~ True.
End TestLexer1.
(* Also, if ``~`` and ``~_h`` are both defined as tokens, the input
``~_ho`` is interpreted as ``~ _ho`` rather than ``~_h o`` so as
not to cut the identifier-like subsequence ``ho``. *)
Section TestLexer2.
Local Notation "~" := not.
Local Notation "~_h" := (fun x => not (not x)).
Local Notation "'_ho'" := False.
Let o := True.
Check ~_ho.
Check ~_h o.
End TestLexer2.
(* Contrastingly, if only ``~_h`` is defined as a token, then ``~_ho``
is an error because no token can be found that includes the whole
subsequence ``ho`` without cutting it in the middle. *)
Section TestLexer3.
Local Notation "~_h" := (fun x => not (not x)).
Fail Check ~_ho.
End TestLexer3.
(* Finally, if all of ``~``, ``~_h`` and ``~_ho`` are defined as
tokens, the input ``~_ho`` is interpreted using the longest match
rule, i.e. as the token ``~_ho``. *)
Section TestLexer4.
Local Notation "~" := not.
Local Notation "~_h" := (fun x => not (not x)).
Local Notation "'_ho'" := False.
Local Notation "~_ho" := True.
Check ~_ho.
End TestLexer4.
|
