summaryrefslogtreecommitdiff
path: root/Common
Commit message (Expand)AuthorAgeFilesLines
* Lean 4.21Andreas Grois2025-11-021-2/+0
* Lean 4.20.1Andreas Grois2025-10-121-1/+0
* Lean 4.19Andreas Grois2025-10-122-4/+4
* Lean 4.18Andreas Grois2025-10-103-9/+10
* Lean 4.16Andreas Grois2025-04-131-1/+1
* Lean 4.15Andreas Grois2025-01-071-1/+1
* Move AStar into a separte library and use it for Day17-1Andreas Grois2025-01-054-319/+1
* Day 17, part 1 (hopefully)Andreas Grois2024-12-224-11/+209
* Continue Day17Andreas Grois2024-12-214-0/+153
* Remove useless simp_wf tactic callsHEADmainAndreas Grois2024-12-171-1/+0
* Day 16 Part 2Andreas Grois2024-12-161-0/+42
* Begin Day16Andreas Grois2024-12-143-0/+20
* Day 14, Part 1.Andreas Grois2024-11-282-0/+14
* Day 13, Part 1Andreas Grois2024-11-251-0/+5
* Day 12 Part 1.Andreas Grois2024-09-241-0/+16
* Continue Day12Andreas Grois2024-09-233-0/+60
* Continue a bit with Day 11 Part 1Andreas Grois2024-09-191-3/+6
* Day 11 ParsingAndreas Grois2024-09-192-24/+99
* Continue Day11/ParsingAndreas Grois2024-09-182-0/+37
* Begin Day 11.Andreas Grois2024-09-181-0/+46
* Day 10, Part 2Andreas Grois2024-09-161-0/+9
* Continue Day10 Part2Andreas Grois2024-09-091-0/+11
* Begin implementing Day10 Part1Andreas Grois2024-09-081-0/+7
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-012-1423/+0
* 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-126-187/+183
* 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