summaryrefslogtreecommitdiff
path: root/Common
Commit message (Collapse)AuthorAgeFilesLines
* Change heap from less-than to less-than-or-equal.Andreas Grois2024-01-131-148/+83
| | | | | This not only simplifies the proofs, it also makes the structure easier to use.
* Fix Heap Insert preserves Heap Proof. Preconditions were wrong.Andreas Grois2024-01-131-18/+59
| | | | | | | | And with wrong I mean "unfulfillable if any elements in the heap should be equal to each other". I'm still not fully happy with this, as it relies on lt being compatible with Eq, but yeah, it works for now.
* 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
| | | | | Finally the propositions about even and odd numbers are no longer decidable. Not that I accidentally use them in runtime code!
* Partial cleanup of HeapAndreas Grois2023-12-182-119/+118
|
* 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-29/+29
|
* BinTreeHeap: Add condition le m nAndreas Grois2023-12-121-19/+51
|
* Incomplete Heap implementation.Andreas Grois2023-12-111-0/+140
|
* Day 8 Part 2Andreas Grois2023-12-092-13/+11
|
* Day 7Andreas Grois2023-12-083-0/+27
|
* Day 6Andreas Grois2023-12-071-0/+4
|
* Allow error messages in parsing (for debugging)Andreas Grois2023-12-071-1/+1
| | | | And fix an off-by-one in day 5
* Day5, part 1Andreas Grois2023-12-061-5/+7
|
* Day 3Andreas Grois2023-12-032-1/+29
|
* Quicksort. Might be useful later.Andreas Grois2023-12-031-0/+24
|
* Day 2Andreas Grois2023-12-021-0/+4
|
* Day 1Andreas Grois2023-12-013-0/+21
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 16:08:11 +0000