From 280a3db6537cd0d760b39b90b9d8515131743bdd Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 28 Jul 2021 16:31:42 -0700 Subject: [PATCH] fix: only print named patterns inside patterns --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 1 + tests/lean/run/PPTopDownAnalyze.lean | 4 +--- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index d042a474f1..b0d50b86f7 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -671,6 +671,7 @@ where @[builtinDelab app.namedPattern] def delabNamedPattern : Delab := do + guard (← read).inPattern guard $ (← getExpr).getAppNumArgs == 3 let x ← withAppFn $ withAppArg delab let p ← withAppArg delab diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 339fce4036..6633f55113 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -227,6 +227,7 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do #testDelabN MonadLift.noConfusionType #testDelabN MonadExcept.noConfusion #testDelabN MonadFinally.noConfusion +#testDelabN Lean.Elab.InfoTree.goalsAt?.match_1 -- TODO: this test is broken because of the inability to solve structural max constraints -- (See https://github.com/leanprover/lean4/issues/590) @@ -237,6 +238,3 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do -- TODO: this is broken because it is currently inaccessible names -- #testDelabN Std.ShareCommon.ObjectMap.find? -- #testDelabN Std.ShareCommon.ObjectMap.insert - --- TODO: these fail because we are not disable named patterns when not using `match` syntax --- #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1