max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: undo workaround

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-07 16:09:42 +02:00
parent 0583970ad8
commit 05b12e2b61
1 changed files with 4 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/BuiltinNotation.lean
View file

@ -67,13 +67,10 @@ open Meta
match stx with
| `(have $[$x :]? $type from $val $[;]? $body) => let x := mkId x; `(let_fun $x : $type := $val; $body)
| `(have $[$x :]? $type by%$b $tac:tacticSeq $[;]? $body) => `(have $[$x :]? $type from by%$b $tac:tacticSeq; $body)
| _ =>
-- TODO: fix `match` syntax, and avoid this workaround
match stx with
| `(have $x:ident : $type:term := $val $[;]? $body) => `(let_fun $x:ident : $type:term := $val; $body)
| `(have $x:ident := $val:term $[;]? $body) => `(let_fun $x:ident := $val:term ; $body)
| `(have $pattern:term := $val:term $[;]? $body) => `(let_fun $pattern:term := $val:term ; $body)
| _ => Macro.throwUnsupported
| `(have $x:ident : $type:term := $val $[;]? $body) => `(let_fun $x:ident : $type:term := $val; $body)
| `(have $x:ident := $val:term $[;]? $body) => `(let_fun $x:ident := $val:term ; $body)
| `(have $pattern:term := $val:term $[;]? $body) => `(let_fun $pattern:term := $val:term ; $body)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
| `(suffices $[$x :]? $type from $val $[;]? $body) => `(have $[$x :]? $type from $body; $val)