From 11f466e3091b34521e48b04e412bbd843bd20d27 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 5 Sep 2024 19:27:36 +0200
Subject: Add for-loop support and update lean toolchain to 4.11

---
 BinaryHeap.lean | 13 +++++++++++++
 lean-toolchain  |  2 +-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index 4c7326f..4f52f23 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -58,6 +58,19 @@ instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) wher
 instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where
   getElem := λ heap index _ ↦ heap.tree.get index
 
+def forM [Monad m] (heap : BinaryHeap α le n) (f : α → m PUnit) : m PUnit :=
+  match n with
+  | .zero => pure ()
+  | .succ _ =>
+    let a := heap.tree.root' --this is faster than pop here, in case of a break.
+    f a >>= λ _ ↦ heap.pop.fst.forM f
+
+instance : ForM m (BinaryHeap α le n) α where
+  forM := BinaryHeap.forM
+
+instance : ForIn m (BinaryHeap α le n) α where
+  forIn := ForM.forIn
+
 /--Helper for the common case of using natural numbers for sorting.-/
 theorem nat_ble_to_heap_le_total : total_le Nat.ble :=
   λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b)
diff --git a/lean-toolchain b/lean-toolchain
index c0eeb78..e74cbdc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.10
+leanprover/lean4:4.11
-- 
cgit v1.2.3