From 894dc0e1b8be7aeb50b465a6d5bfaff99f48cfe5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Feb 2022 10:19:04 +0100
Subject: [PATCH] fix: pretty-printing `match` dependent on `let`

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean |  3 ++-
 tests/lean/{run => }/heapSort.lean               |  0
 tests/lean/heapSort.lean.expected.out            | 11 +++++++++++
 3 files changed, 13 insertions(+), 1 deletion(-)
 rename tests/lean/{run => }/heapSort.lean (100%)
 create mode 100644 tests/lean/heapSort.lean.expected.out

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 2ca7e719f4..a5a11cef17 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -311,7 +311,8 @@ structure AppMatchState where
 private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Syntax)) :=
   withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do
     let ty ← instantiateForall st.matcherTy st.params
-    forallTelescope ty fun params _ => do
+    -- need to reduce `let`s that are lifted into the matcher type
+    forallTelescopeReducing ty fun params _ => do
       -- skip motive and discriminators
       let alts := Array.ofSubarray params[1 + st.discrs.size:]
       alts.mapIdxM fun idx alt => do
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/heapSort.lean
similarity index 100%
rename from tests/lean/run/heapSort.lean
rename to tests/lean/heapSort.lean
diff --git a/tests/lean/heapSort.lean.expected.out b/tests/lean/heapSort.lean.expected.out
new file mode 100644
index 0000000000..ab411359bb
--- /dev/null
+++ b/tests/lean/heapSort.lean.expected.out
@@ -0,0 +1,11 @@
+heapSort.lean:32:28-32:33: warning: declaration uses 'sorry'
+heapSort.lean:51:22-51:27: warning: declaration uses 'sorry'
+heapSort.lean:61:30-61:35: warning: declaration uses 'sorry'
+heapSort.lean:110:29-110:34: warning: declaration uses 'sorry'
+@Array.heapSort.loop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α),
+  Array.heapSort.loop lt a out =
+    match BinaryHeap.max a, (_ : BinaryHeap.max a = BinaryHeap.max a) with
+    | none, e => out
+    | some x, e =>
+      let_fun this := (_ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a);
+      Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)