From feb71271e990d4fe937d2d6c99d87cd0179ce2b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 31 Jul 2022 05:27:37 -0700 Subject: [PATCH] fix: remove redundant alternatives --- src/Init/NotationExtra.lean | 2 -- src/Lean/Elab/Quotation/Precheck.lean | 3 +-- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 1ddf433e1f..43ba9bfa40 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -92,11 +92,9 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander | `($(_)) => `(()) - | _ => throw () @[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander | `($(_)) => `([]) - | _ => throw () @[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander | `($(_) $x []) => `([$x]) diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index c4e6c42a3e..f0ac3bd9d6 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -112,9 +112,8 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do for arg in args.raw do match arg with | `(argument| ($_ := $e)) => precheck e - | `(argument| $e:term) => precheck e | `(argument| ..) => pure () - | _ => throwUnsupportedSyntax + | `(argument| $e:term) => precheck e | _ => throwUnsupportedSyntax @[builtinQuotPrecheck Lean.Parser.Term.paren] def precheckParen : Precheck