From cc1dcf804359276f0f7e8a673c04b2a2b7d69951 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 2 Jan 2024 04:36:39 -0500
Subject: [PATCH] feat: delaborate `have` inside `do` blocks (#3116)

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 10 ++++++++++
 tests/lean/delabDoLetFun.lean                    | 14 ++++++++++++++
 tests/lean/delabDoLetFun.lean.expected.out       |  6 ++++++
 3 files changed, 30 insertions(+)
 create mode 100644 tests/lean/delabDoLetFun.lean
 create mode 100644 tests/lean/delabDoLetFun.lean.expected.out

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index cd52a32514..ba547db886 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -753,6 +753,16 @@ partial def delabDoElems : DelabM (List Syntax) := do
       let b := b.instantiate1 fvar
       descend b 2 $
         prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
+  else if e.isLetFun then
+    -- letFun.{u, v} : {α : Sort u} → {β : α → Sort v} → (v : α) → ((x : α) → β x) → β v
+    let stxT ← withNaryArg 0 delab
+    let stxV ← withNaryArg 2 delab
+    withAppArg do
+      match (← getExpr) with
+      | Expr.lam .. =>
+        withBindingBodyUnusedName fun n => do
+          prependAndRec `(doElem|have $n:term : $stxT := $stxV)
+      | _ => failure
   else
     let stx ← delab
     return [← `(doElem|$stx:term)]
diff --git a/tests/lean/delabDoLetFun.lean b/tests/lean/delabDoLetFun.lean
new file mode 100644
index 0000000000..4c6fcfb4ed
--- /dev/null
+++ b/tests/lean/delabDoLetFun.lean
@@ -0,0 +1,14 @@
+/-!
+Testing delaboration of `letFun` as a `doElem`
+-/
+
+/-!
+A `have` in the middle of a `do` expression.
+-/
+def x : IO Nat := do
+  println! "a"
+  have a := 1
+  println! "b"
+  return a
+
+#print x
diff --git a/tests/lean/delabDoLetFun.lean.expected.out b/tests/lean/delabDoLetFun.lean.expected.out
new file mode 100644
index 0000000000..88a4763dae
--- /dev/null
+++ b/tests/lean/delabDoLetFun.lean.expected.out
@@ -0,0 +1,6 @@
+def x : IO Nat :=
+do
+  IO.println (toString "a")
+  have a : Nat := 1
+  IO.println (toString "b")
+  pure a