19e4c30542
We can now write ```lean syntax "case!" ident ":" term "with" term "," term : term macro_rules | `(case! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e) ``` Before the series of commits to change `let` syntax, the quasiquotation `(let $h := $c; cond $h $t $e) produced the weird error message "`;` expected" at ":=". The problem was that $h was matching the now deleted "nonterminal" ```lean def letIdDecl := parser! try (letIdLhs >> " := ") >> termParser ``` This was not a bug, but a side-effect on how the `let` syntax was declared. cc @kha
19 lines
477 B
Text
19 lines
477 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 : $c with $t, $e) => `((fun $h => cond $h $t $e) $c)
|
|
|
|
#check case! h : 0 == 0 with h, not h
|
|
|
|
syntax "case2!" ident ":" term "with" term "," term : term
|
|
macro_rules
|
|
| `(case2! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e)
|
|
|
|
#check case2! h : 0 == 0 with h, not h
|