From 7ca2f70c2f977ca42c9df1acea86a9aa4e872928 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 14 May 2021 18:36:59 +0200
Subject: [PATCH] feat: Eq.rec delaborator

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean |  5 +++++
 tests/lean/ppProofs.lean                         |  1 +
 tests/lean/ppProofs.lean.expected.out            | 10 ++++++++--
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 867404918f..fdd606fede 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -629,4 +629,9 @@ def delabEqNDRec : Delab := whenPPOption getPPNotation do
   let h ← withAppArg delab
   `($h ▸ $m)
 
+@[builtinDelab app.Eq.rec]
+def delabEqRec : Delab := whenPPOption getPPNotation do
+  -- relevant signature parts as in `Eq.ndrec`
+  delabEqNDRec
+
 end Lean.PrettyPrinter.Delaborator
diff --git a/tests/lean/ppProofs.lean b/tests/lean/ppProofs.lean
index 21e5372693..b730d3b35b 100644
--- a/tests/lean/ppProofs.lean
+++ b/tests/lean/ppProofs.lean
@@ -1,5 +1,6 @@
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
+example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp
 set_option pp.proofs.withType false
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 set_option pp.proofs true
diff --git a/tests/lean/ppProofs.lean.expected.out b/tests/lean/ppProofs.lean.expected.out
index 0ef842f7dd..3e0a00a1d7 100644
--- a/tests/lean/ppProofs.lean.expected.out
+++ b/tests/lean/ppProofs.lean.expected.out
@@ -12,14 +12,20 @@ b : β
 a : α
 h : α = β
 ⊢ (_ : α = β) ▸ a = b
-ppProofs.lean:4:50-4:51: error: don't know how to synthesize placeholder
+ppProofs.lean:3:50-3:57: error: unsolved goals
+α β : Sort ?u
+b : β
+a : α
+h : α = β
+⊢ (_ : α = β) ▸ a = b
+ppProofs.lean:5:50-5:51: error: don't know how to synthesize placeholder
 context:
 α β : Sort u_1
 b : β
 a : α
 h : α = β
 ⊢ _ ▸ a = b
-ppProofs.lean:6:50-6:51: error: don't know how to synthesize placeholder
+ppProofs.lean:7:50-7:51: error: don't know how to synthesize placeholder
 context:
 α β : Sort u_1
 b : β