bdb9f4c86e
@Kha this commit fix another example of weird error message I have experienced in the last few days. The macro ```lean syntax "case!" ident ":" term "with" term "," term : term macro_rules | `(case! $h : $cond with $t, $e) => `((fun $h => cond $h $t $e) $cond) ``` is accepted, but as in `fun` binders, we get a weird error when trying to elaborate an instance of the macro. Example: ```lean check case! h : 0 == 0 with h, not h ```
13 lines
305 B
Text
13 lines
305 B
Text
new_frontend
|
|
|
|
syntax "[" ident "↦" term "]" : term
|
|
macro_rules
|
|
| `([$x ↦ $v]) => `(fun $x => $v)
|
|
|
|
#check [x ↦ x + 1]
|
|
|
|
syntax "case!" ident ":" term "with" term "," term : term
|
|
macro_rules
|
|
| `(case! $h : $cond with $t, $e) => `((fun $h => cond $h $t $e) $cond)
|
|
|
|
#check case! h : 0 == 0 with h, not h
|