feat: Eq.rec delaborator

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

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

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 : β