-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathnotations.t
139 lines (90 loc) · 3.85 KB
/
notations.t
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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
Testing notation commands
$ narya -v -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y := f x y' -e 'def ff (x y : A) : A := x & y' -e 'axiom a : A' -e 'echo ff a a'
￫ info[I0001]
￮ axiom A assumed
￫ info[I0001]
￮ axiom f assumed
￫ info[I0002]
￮ notation f defined
￫ info[I0000]
￮ constant ff defined
￫ info[I0001]
￮ axiom a assumed
a & a
: A
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y.z := f x y.z'
￫ error[E0202]
￮ invalid local variable name: y.z
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "/" := f x x'
￫ error[E2207]
￮ notation variable 'x' used twice
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y "#" z := f x y'
￫ error[E2206]
￮ unused notation variable: 'z'
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "/" := f x y'
￫ error[E2208]
￮ unbound variable(s) in notation definition: y
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y "#" x := f x y'
￫ error[E2204]
￮ duplicate notation variable: 'x'
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation f : "#" x "&" y "#" := f x y'
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation f : x "&" y "#" := f x y'
￫ error[E2203]
￮ notation command doesn't match pattern (tightness must be omitted only for outfix notations)
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : "#" x "&" y "#" := f x y'
￫ error[E2203]
￮ notation command doesn't match pattern (tightness must be omitted only for outfix notations)
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0.5 f : x "&" y := f x y' -e 'def ff (x y : A) : A := x & y'
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0.1 f : x "&" y := f x y'
￫ error[E2200]
￭ command-line exec string
1 | notation 0.1 f : x "&" y := f x y
^ invalid tightness: 0.1
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&x" y := f x y'
￫ error[E2201]
￮ invalid notation symbol: &x
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y := Type x y'
￫ error[E2205]
￮ invalid notation head: Type
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A' -e 'notation f : "&" := f'
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" … "&" y := f x y'
￫ error[E0100]
￮ internal ellipses in notation not yet implemented
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" … y := f x y'
￫ error[E0100]
￮ internal ellipses in notation not yet implemented
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : … := f x y'
￫ error[E2202]
￮ invalid notation pattern: has no symbols
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : … x "&" y … := f x y'
￫ error[E2202]
￮ invalid notation pattern: can't be both right and left associative
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A' -e 'notation 0 f : x := f x'
￫ error[E2202]
￮ invalid notation pattern: has no symbols
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : "&" x y := f x y'
￫ error[E2202]
￮ invalid notation pattern: missing symbol between variables
[1]
$ narya -e 'axiom A:Type' -e 'axiom f:A->A->A' -e 'notation 0 f : x "&" y := f x y' -e 'notation 0 f2 : x "%" y := f x y' -e 'def ff (x y : A) : A := x & y' -e 'def ff2 (x y : A) : A := x % y' -e 'axiom a : A' -e 'echo ff a a' -e 'echo ff2 a a'
￫ warning[E2209]
￮ replacing printing notation for f (previous notation will still be parseable)
a % a
: A
a % a
: A