From a21265281b8092345f80016ab3d16e9246cd176f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Jan 2022 12:55:28 -0800 Subject: [PATCH] chore: remove temporary workaround --- src/Init/Prelude.lean | 3 --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 10 ---------- 2 files changed, 13 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index cbe06624fe..e9038f79f1 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -170,9 +170,6 @@ structure Subtype {α : Sort u} (p : α → Prop) where /-- Auxiliary Declaration used to implement the notation (a : α) -/ @[reducible] def typedExpr (α : Sort u) (a : α) : α := a --- TODO: delete -@[reducible] def namedPatternOld {α : Sort u} (x a : α) : α := a - /-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/ @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 3b0e7a74cf..6df1bbb724 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -685,16 +685,6 @@ where | none => withBindingBodyUnusedName fun h => do return (← delab, h.getId) -@[builtinDelab app.namedPatternOld] -def delabNamedPatternOld : Delab := do - -- Note: we keep this as a delaborator because it accesses the DelabM context - guard (← read).inPattern - guard $ (← getExpr).getAppNumArgs == 3 - let x ← withAppFn $ withAppArg delab - let p ← withAppArg delab - guard x.isIdent - `($x:ident@$p:term) - @[builtinDelab app.namedPattern] def delabNamedPattern : Delab := do -- Note: we keep this as a delaborator because it accesses the DelabM context