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
|
File "./output/NotationSyntax.v", line 2, characters 38-50:
The command has indeed failed with message:
"only parsing" is given more than once.
File "./output/NotationSyntax.v", line 3, characters 38-51:
The command has indeed failed with message:
A notation cannot be both "only printing" and "only parsing".
File "./output/NotationSyntax.v", line 4, characters 39-52:
The command has indeed failed with message:
"only printing" is given more than once.
File "./output/NotationSyntax.v", line 5, characters 33-43:
Warning: The format modifier is irrelevant for only-parsing rules.
[irrelevant-format-only-parsing,parsing,default]
File "./output/NotationSyntax.v", line 8, characters 20-30:
Warning:
Notations for numbers or strings are primitive; skipping this modifier.
[primitive-token-modifier,parsing,default]
1%nat
: nat
File "./output/NotationSyntax.v", line 10, characters 23-26:
The command has indeed failed with message:
Notations for numbers or strings are primitive and need not be reserved.
File "./output/NotationSyntax.v", line 12, characters 25-35:
Warning:
Notations for numbers or strings are primitive; skipping this modifier.
[primitive-token-modifier,parsing,default]
"tt"
: unit
"tt"%string
: string
File "./output/NotationSyntax.v", line 16, characters 23-31:
The command has indeed failed with message:
Notations for numbers or strings are primitive and need not be reserved.
"t""t"
: unit
# "|" true
: option bool
"|"%string
: string
2 "|" 4
: nat * nat
"I'm true"
: bool
""
: bool
symbolwith"doublequote
: bool
"
: bool
|
