From 3b3e54143c685305b9a5056d004a0da0ffedf2db Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 29 Jul 2021 12:27:06 -0700 Subject: [PATCH] feat: pp.analyze isSubstLike support Eq.rec --- src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +- tests/lean/ppProofs.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 3cfc7d8d70..312ea2e08b 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -216,7 +216,7 @@ def isFunLike (e : Expr) : MetaM Bool := do withTransparency TransparencyMode.all do forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0 def isSubstLike (e : Expr) : Bool := - e.isAppOfArity `Eq.ndrec 6 + e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6 def nameNotRoundtrippable (n : Name) : Bool := n.hasMacroScopes || isPrivateName n || containsNum n diff --git a/tests/lean/ppProofs.lean b/tests/lean/ppProofs.lean index b730d3b35b..35ce06374f 100644 --- a/tests/lean/ppProofs.lean +++ b/tests/lean/ppProofs.lean @@ -1,3 +1,5 @@ +set_option pp.analyze.trustSubst true +set_option pp.proofs false example (h : α = β) : h ▸ (a : α) = (b : β) := _ example (h : α = β) : id h ▸ (a : α) = (b : β) := _ example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp