You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
The term {deftech}_notation_ is used in two ways in Lean: it can refer to the general concept of concise ways of writing down ideas, and it is the name of a language feature that allows notations to be conveniently implemented with little code.
28
32
Like custom operators, Lean notations allow the grammar of terms to be extended with new forms.
29
33
However, notations are more general: the new syntax may freely intermix required keywords or operators with subterms, and they provide more precise control over precedence levels.
30
34
Notations may also rearrange their parameters in the resulting subterms, while infix operators provide them to the function term in a fixed order.
31
35
Because notations may define operators that use a mix of prefix, infix, and postfix components, they can be called {deftech}_mixfix_ operators.
The body of a notation definition consists of a sequence of {deftech}_notation items_, which may be either string literals or identifiers with optional precedences.
As with operator declarations, the contents of the documentation comments are shown to users while they interact with the new syntax.
54
73
Adding the {attr}`inherit_doc` attribute causes the documentation comment of the function at the head of the term into which the notation expands to be copied to the new syntax.
55
74
Other attributes may be added to invoke other compile-time metaprograms on the resulting definition.
Notations interact with {tech}[section scopes] in the same manner as attributes and operators.
58
82
By default, notations are available in any module that transitively imports the one in which they are established, but they may be declared `scoped` or `local` to restrict their availability either to contexts in which the current namespace has been opened or to the current {tech}[section scope], respectively.
Like operators, the {tech}[local longest-match rule] is used while parsing notations.
61
90
If more than one notation ties for the longest match, the declared priorities are used to determine which parse result applies.
62
91
If this still does not resolve the ambiguity, then all are saved, and the elaborator is expected to attempt all of them, succeeding when exactly one can be elaborated.
Rather than a single operator with its fixity and token, the body of a notation declaration consists of a sequence of {deftech}_notation items_, which may be either new {tech}[atoms] (including both keywords such as `if`,`#eval`, or `where` and symbols such as `=>`,`+`,`↗`,`⟦`, or `⋉`) or positions for terms.
65
99
Just as they doin operators, string literals identify the placement of atoms.
66
-
Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntaxin {tech}[証明状態]proof states and error messages.
100
+
Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntaxin {tech}[proof states] and error messages.
67
101
Identifiers indicate positions where terms are expected, and name the corresponding term so it can be inserted in the notation's expansion.
While custom operators have a single notion of precedence, there are many involved in a notation.
70
109
The notation itself has a precedence, as does each term to be parsed.
71
110
The notation's precedence determines which contexts it may be parsed in: the parser only attempts to parse productions whose precedence is at least as high as the current context.
72
111
For example, because multiplication has higher precedence than addition, the parser will attempt to parse an infix multiplication term while parsing the arguments to addition, but not vice versa.
73
112
The precedence of each term to be parsed determines which other productions may occur in them.
If no precedence is supplied for the notation itself, the default value depends on the form of the notation.
76
120
If the notation both begins and ends with an atom (represented by string literals), then the default precedence is `max`.{TODO}[keywordOf]
77
121
This applies both to notations that consist only of a single atom and to notations with multiple items, in which the first and last items are both atoms.
78
122
Otherwise, the default precedence of the whole notation is `lead`.
79
123
If no precedence is provided fornotation items that are terms, then they default to precedence `min`.
After the required double arrow ({keywordOf Lean.Parser.Command.notation}`=>`), the notation is provided with an expansion.
129
178
While operators are always expanded by applying their function to the operator's arguments in order, notations may place their term items in any position in the expansion.
130
179
The terms are referred to by name.
131
180
Term items may occur any number of times in the expansion.
132
181
Because notation expansion is a purely syntactic process that occurs prior to elaboration or code generation, duplicating terms in the expansion may lead to duplicated computation when the resulting term is evaluated, or even duplicated side effects when working in a monad.
notation (name := ignore) "ignore " _ign:arg e:arg => e
139
200
```
140
201
202
+
:::comment
141
203
The term in the ignored position is discarded, and Lean never attempts to elaborate it, so terms that would otherwise result in errors can be used here:
However, the ignored term must still be syntactically valid:
217
+
:::
218
+
219
+
しかし、無視される項は構文的に有効でなければなりません：
220
+
150
221
```syntaxError ignore' (category := command)
151
222
#eval ignore (2 +) 5
152
223
```
153
224
```leanOutput ignore'
154
225
<example>:1:17: expected term
155
226
```
156
-
:::
157
227
::::
228
+
:::::
158
229
159
-
::::keepEnv
160
-
:::example"Duplicated Terms in Notation Expansion"
230
+
:::::keepEnv
231
+
:::comment
232
+
::example"Duplicated Terms in Notation Expansion"
233
+
:::
234
+
::::example"記法展開で複製された項"
161
235
236
+
:::comment
162
237
The {keywordOf dup}`dup!`notation duplicates its sub-term.
163
238
239
+
:::
240
+
241
+
{keywordOf dup}`dup!` 記法はその部分項を複製しています。
242
+
164
243
```lean
165
244
notation (name := dup) "dup!" t:arg => (t, t)
166
245
```
167
246
247
+
:::comment
168
248
Because the term is duplicated, it can be elaborated separately with different types:
249
+
:::
250
+
251
+
この項は複製されているため、異なる型で別々にエラボレートされることができます：
252
+
169
253
```lean
170
254
defe : Nat × Int := dup! (2 + 2)
171
255
```
172
256
257
+
:::comment
173
258
Printing the resulting definition demonstrates that the work of addition will be performed twice:
259
+
:::
260
+
261
+
この定義を表示すると、加算が2回行われていることがわかります：
262
+
174
263
```lean (name := dup)
175
264
#print e
176
265
```
177
266
```leanOutput dup
178
267
defe : Nat × Int :=
179
268
(2 + 2, 2 + 2)
180
269
```
181
-
:::
182
270
::::
271
+
:::::
183
272
184
273
274
+
:::comment
185
275
When the expansion consists of the application of a function defined in the global environment and each term in the notation occurs exactly once, an {tech}[unexpander] is generated.
186
-
The new notation will be displayed in {tech}[証明状態]proof states, error messages, and other output from Lean when matching function application terms otherwise would have been displayed.
276
+
The new notation will be displayed in {tech}[proof states], error messages, and other output from Lean when matching function application terms otherwise would have been displayed.
187
277
As with custom operators, Lean does not track whether the notation was used in the original term; it is used at every opportunity in Lean's output.
Internally, operator declarations are translated into notation declarations.
195
295
Term notation items are inserted where the operator would expect arguments, and in the corresponding positions in the expansion.
196
296
For prefix and postfix operators, the notation's precedence as well as the precedences of its term items is the operator's declared precedence.
197
297
For non-associative infix operators, the notation's precedence is the declared precedence, but both arguments are parsed at a precedence level that is one higher, which prevents successive uses of the notation without parentheses.
198
298
Associative infix operators use the operator's precedence for the notation and for one argument, while a precedence that is one level higher is used for the other argument; this prevents successive applications in one direction only.
199
299
Left-associative operators use the higher precedence for their right argument, while right-associative operators use the higher precedence for their left argument.
0 commit comments