summaryrefslogtreecommitdiff
path: root/Common/Nat.lean
Commit message (Collapse)AuthorAgeFilesLines
* Continue Day12Andreas Grois2024-09-231-0/+4
|
* Day 11 ParsingAndreas Grois2024-09-191-0/+13
|
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-011-172/+0
|
* Squashed commit of the following:Andreas Grois2024-07-121-17/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 21:59:44 2024 +0200 Finish Lean 4.9 update. commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6 Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 21:40:21 2024 +0200 Lean 4.9 upgrade, heap is where it was before... commit db34881e21391c96a6a0b939552b0f6f77d05bd8 Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 00:31:22 2024 +0200 Further Lean 4.9 compat... commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214 Author: Andreas Grois <andi@grois.info> Date: Thu Jul 11 22:15:11 2024 +0200 Further Lean 4.9 porting commit a4ace32cbb02959f9625578b511c2486e0816367 Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 23:18:29 2024 +0200 Continue porting to Lean 4.9 commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 23:10:34 2024 +0200 Continue port to Lean 4.9 commit 835ce644b97840048de0df40676ff6f3a8b99985 Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 22:14:59 2024 +0200 Partial port to Lean 4.9. Not compiling yet.
* Continue on CompleteTree.heapReplaceElementAtIsHeapAndreas Grois2024-07-101-0/+7
|
* Finish CompleteTree.get implementation. Not proven to be correct yet.Andreas Grois2024-06-301-0/+8
|
* Partial implementation of CompleteTree.removeAtIndexAndreas Grois2024-06-301-0/+9
|
* Even more cleanup in HeapAndreas Grois2023-12-181-0/+6
|
* More cleanup of code in BinaryHeap.Andreas Grois2023-12-181-0/+60
| | | | | 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-181-0/+93
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 17:55:41 +0000