summaryrefslogtreecommitdiff
path: root/Common/BinaryHeap.lean
Commit message (Expand)AuthorAgeFilesLines
* (Finally) rename BalancedTree to CompleteTreeAndreas Grois2024-01-101-52/+52
* Implement actual BinaryHeap.insert function.Andreas Grois2024-01-101-0/+6
* Proof that heap insert preserves a heap is done!Andreas Grois2024-01-101-3/+73
* Heap.insert: Insert-Left is proven now.Andreas Grois2024-01-101-7/+45
* More progress on heap.insert proofAndreas Grois2024-01-091-8/+25
* Further progress on heap insert proof.Andreas Grois2024-01-081-12/+10
* Progress on the proof that heap.insert keeps the heap intact.Andreas Grois2024-01-081-0/+17
* Unfinished proof that insert keeps heap a heapAndreas Grois2024-01-051-31/+99
* Even more cleanup in HeapAndreas Grois2023-12-181-6/+0
* More cleanup of code in BinaryHeap.Andreas Grois2023-12-181-55/+1
* Partial cleanup of HeapAndreas Grois2023-12-181-119/+25
* Heap now has balancing conditions completeAndreas Grois2023-12-181-18/+174
* Heap: At least one subtree needs to be perfect now.Andreas Grois2023-12-151-13/+113
* Rename file to BinaryHeap, as it isn't a BTreeAndreas Grois2023-12-131-0/+172
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 16:56:35 +0000