0dcdc2c198
@kha, the implementation is a little bit hackish. It is whitespace sensitive to avoid `f @g`, an application with argument `@g` to be parsed as a named pattern. Here are other approaches I have considered: 1- In the `namedPattern`, we add a guard that ensures the pattern is *not* an identifier. Thus, `f @g` would not be considered a valid `namedPattern`. Drawback: we would always try to parse it as a namedPattern first, fail, and then try as an application. 2- Enforce whitespace before application arguments. Drawback: `f(a+b)` would not be a valid application anymore. |
||
|---|---|---|
| .. | ||
| control | ||
| data | ||
| lean | ||
| coe.lean | ||
| core.lean | ||
| default.lean | ||
| fix.lean | ||
| init.md | ||
| io.lean | ||
| platform.lean | ||
| util.lean | ||
| wf.lean | ||