From 05b12e2b612c3c7d5f41d87936142c0ba31948dc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 7 May 2021 16:09:42 +0200 Subject: [PATCH] chore: undo workaround --- src/Lean/Elab/BuiltinNotation.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 4d1dc9018b..6f27c9ccd4 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -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)