summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Finish CompleteTree.heapReplaceRootIsHeap.Andreas Grois2024-07-141-9/+42
* Continue proof for heapReplaceRootIsHeap (heapReplaceElementAtIsHeap)Andreas Grois2024-07-131-7/+56
* Squashed commit of the following:Andreas Grois2024-07-1210-192/+190
* Continue on CompleteTree.heapReplaceElementAtIsHeapAndreas Grois2024-07-102-9/+217
* Finish CompleteTree.get implementation. Not proven to be correct yet.Andreas Grois2024-06-302-6/+15
* partial implementation of CompleteTree.getAndreas Grois2024-06-301-0/+18
* CompleteTree.replaceElementAt finished - now needs proofAndreas Grois2024-06-301-22/+40
* Partial implementation of CompleteTree.removeAtIndexAndreas Grois2024-06-302-3/+66
* CompleteTree.popLastIsHeap finished.Andreas Grois2024-06-291-2/+14
* Continue on popLast proof. popLastLeavesRoot finished.Andreas Grois2024-06-281-13/+59
* Continue on popLast validity proof. Still incomplete.Andreas Grois2024-06-271-5/+57
* Heap: Trivial part of popLastIsHeap proof.Andreas Grois2024-03-311-0/+16
* Make BinaryTree.PopLast function work with unfoldAndreas Grois2024-01-301-32/+34
* Make Find function take a predicate. Simplify PopLast.Andreas Grois2024-01-251-27/+26
* Minor, rename wellDefinedLt to wellDefinedLeAndreas Grois2024-01-131-4/+4
* Change heap from less-than to less-than-or-equal.Andreas Grois2024-01-131-148/+83
* Fix Heap Insert preserves Heap Proof. Preconditions were wrong.Andreas Grois2024-01-131-18/+59
* Rename not_equal to antisymm, because that's what it is.Andreas Grois2024-01-101-7/+7
* (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-182-6/+6
* More cleanup of code in BinaryHeap.Andreas Grois2023-12-182-55/+61
* Partial cleanup of HeapAndreas Grois2023-12-183-119/+119
* 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-132-30/+30
* BinTreeHeap: Add condition le m nAndreas Grois2023-12-121-19/+51
* Incomplete Heap implementation.Andreas Grois2023-12-115-8/+146
* Day9: Simplify proof of terminationAndreas Grois2023-12-091-1/+1
* Day 9Andreas Grois2023-12-094-18/+284
* Fix Day 8 Part 2: Forgot to un-comment something.Andreas Grois2023-12-091-2/+2
* Day 8 Part 2Andreas Grois2023-12-095-17/+156
* Not working Day8 Part 2.Andreas Grois2023-12-082-21/+52
* Day 8 Part 1Andreas Grois2023-12-084-2/+893
* Day 7Andreas Grois2023-12-088-0/+1243
* Day 6Andreas Grois2023-12-073-9/+82
* Allow error messages in parsing (for debugging)Andreas Grois2023-12-0710-33/+62
* Part 2, finallyAndreas Grois2023-12-062-17/+66
* Part of Day5 Part 2Andreas Grois2023-12-061-54/+105
* Day5, part 1Andreas Grois2023-12-065-5/+475
* Day 4Andreas Grois2023-12-044-0/+277
* Day 3: Fix swapped adjacents.Andreas Grois2023-12-031-11/+11
* Day 3, minor cleanupAndreas Grois2023-12-031-31/+12
* Day 3Andreas Grois2023-12-038-1/+319
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 16:52:34 +0000