feat: delaborate have inside do blocks (#3116)

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)]

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

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