summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Continue Day10 Part 2Andreas Grois2024-09-111-24/+68
* Continue Day10 Part 2.Andreas Grois2024-09-111-48/+67
* Continue Day10 Part2Andreas Grois2024-09-111-12/+103
* Continue Day10 Part2Andreas Grois2024-09-101-36/+86
* Continue a bit on Day10 Part2Andreas Grois2024-09-101-17/+61
* Continue Day10 Part2Andreas Grois2024-09-093-6/+66
* Begin Day 10 Part 2Andreas Grois2024-09-081-11/+38
* Fix issue in Day10 Part1 end condition.Andreas Grois2024-09-081-1/+1
* Day 10 Part 1Andreas Grois2024-09-082-52/+76
* Begin implementing Day10 Part1Andreas Grois2024-09-082-34/+351
* Day 10 Parsing. If I don' want to prove the inverse, it's done.Andreas Grois2024-09-071-6/+100
* Parser for Day10, maybe done.Andreas Grois2024-09-053-14/+138
* Continue day10 input parsing proofsAndreas Grois2024-09-051-4/+80
* Contineu Area.ParseRaw_start_positionAndreas Grois2024-09-041-3/+19
* Unfinished rewrite of Area.parseAndreas Grois2024-09-041-45/+299
* First draft of input-parsing function for Day 10.Andreas Grois2024-09-022-1/+251
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-015-1426/+4
* Heap: Nomenclature and namespace changes.Andreas Grois2024-07-211-25/+25
* Simplify CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-78/+32
* Finish CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-1/+105
* Heap: Unfinished proof RemoveLastWithIndex returns consistent data.Andreas Grois2024-07-201-0/+34
* Minor: Replace some simp by simp only in BinaryHeapAndreas Grois2024-07-201-57/+61
* Remove CompleteTree.indexOfLast, add CompleteTree.heapRemoveLastWithIndexAndreas Grois2024-07-201-60/+77
* Heap: Further nomenclature improvements.Andreas Grois2024-07-191-28/+28
* Make CompleteTree.heapRemoveLast private.Andreas Grois2024-07-191-40/+38
* Heap: Nomenclature clarified. Push and Pop now do what is expected.Andreas Grois2024-07-191-111/+111
* Heap: Exchange return values of the remove/replace functions.Andreas Grois2024-07-191-56/+56
* Factor out proofs of CompleteTree.popLast for readabilityAndreas Grois2024-07-191-52/+44
* Heap: Minor cleanup. Do a TODO.Andreas Grois2024-07-171-92/+68
* Finish BinaryHeap.RemoveAt.Andreas Grois2024-07-161-25/+119
* Continue on CompleteTree.heapReplaceElementAtIsHeap. Nearly done.Andreas Grois2024-07-151-13/+72
* Further work on heapReplaceElementAtIsHeapAndreas Grois2024-07-141-2/+23
* Continue at CompleteTree.heapReplaceElementAtIsHeapAndreas Grois2024-07-141-1/+22
* BinaryHeap.RemoveRoot added, and some proofs cleaned up a bitAndreas Grois2024-07-141-22/+26
* 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
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 13:30:04 +0000