| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Heap: Trivial part of popLastIsHeap proof. | Andreas Grois | 2024-03-31 | 1 | -0/+16 |
| | | |||||
| * | Make BinaryTree.PopLast function work with unfold | Andreas Grois | 2024-01-30 | 1 | -32/+34 |
| | | | | | at the cost of making it harder to read. | ||||
| * | Make Find function take a predicate. Simplify PopLast. | Andreas Grois | 2024-01-25 | 1 | -27/+26 |
| | | |||||
| * | Minor, rename wellDefinedLt to wellDefinedLe | Andreas Grois | 2024-01-13 | 1 | -4/+4 |
| | | |||||
| * | Change heap from less-than to less-than-or-equal. | Andreas Grois | 2024-01-13 | 1 | -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 Grois | 2024-01-13 | 1 | -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 Grois | 2024-01-10 | 1 | -7/+7 |
| | | |||||
| * | (Finally) rename BalancedTree to CompleteTree | Andreas Grois | 2024-01-10 | 1 | -52/+52 |
| | | |||||
| * | Implement actual BinaryHeap.insert function. | Andreas Grois | 2024-01-10 | 1 | -0/+6 |
| | | |||||
| * | Proof that heap insert preserves a heap is done! | Andreas Grois | 2024-01-10 | 1 | -3/+73 |
| | | |||||
| * | Heap.insert: Insert-Left is proven now. | Andreas Grois | 2024-01-10 | 1 | -7/+45 |
| | | |||||
| * | More progress on heap.insert proof | Andreas Grois | 2024-01-09 | 1 | -8/+25 |
| | | |||||
| * | Further progress on heap insert proof. | Andreas Grois | 2024-01-08 | 1 | -12/+10 |
| | | |||||
| * | Progress on the proof that heap.insert keeps the heap intact. | Andreas Grois | 2024-01-08 | 1 | -0/+17 |
| | | |||||
| * | Unfinished proof that insert keeps heap a heap | Andreas Grois | 2024-01-05 | 1 | -31/+99 |
| | | |||||
| * | Even more cleanup in Heap | Andreas Grois | 2023-12-18 | 1 | -6/+0 |
| | | |||||
| * | More cleanup of code in BinaryHeap. | Andreas Grois | 2023-12-18 | 1 | -55/+1 |
| | | | | | | Finally the propositions about even and odd numbers are no longer decidable. Not that I accidentally use them in runtime code! | ||||
| * | Partial cleanup of Heap | Andreas Grois | 2023-12-18 | 1 | -119/+25 |
| | | |||||
| * | Heap now has balancing conditions complete | Andreas Grois | 2023-12-18 | 1 | -18/+174 |
| | | |||||
| * | Heap: At least one subtree needs to be perfect now. | Andreas Grois | 2023-12-15 | 1 | -13/+113 |
| | | |||||
| * | Rename file to BinaryHeap, as it isn't a BTree | Andreas Grois | 2023-12-13 | 1 | -0/+172 |
 |
index : aoc-2023 | |
| Advent of Code 2023 - I'm still learning Lean4, so please don't judge. | Andreas Grois |
| summaryrefslogtreecommitdiff |