From 6627e81d169ed73a3f714cceedcd10ae58b26803 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 10 Jan 2024 21:01:38 +0100
Subject: Implement actual BinaryHeap.insert function.

---
 Common/BinaryHeap.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Common')

diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean
index 5f08b43..c2f1901 100644
--- a/Common/BinaryHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -344,6 +344,12 @@ theorem BalancedTree.heapInsertIsHeap {elem : α} {heap : BalancedTree α o} {lt
           case inr.zero => contradiction
           case inr.succ => simp[h₈]
 
+def BinaryHeap.insert {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1)
+| elem, BinaryHeap.mk tree valid wellDefinedLt =>
+  let valid := tree.heapInsertIsHeap valid wellDefinedLt
+  let tree := tree.heapInsert lt elem
+  {tree, valid, wellDefinedLt}
+
 /--Helper function for BalancedTree.indexOf.-/
 def BalancedTree.indexOfAux {α : Type u} [BEq α] (elem : α) (heap : BalancedTree α o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) :=
   match o, heap with
-- 
cgit v1.2.3