| Branch | Commit message | Author | Age | |
|---|---|---|---|---|
| main | Proof that toList has the same length as the heap. | Andreas Grois | 5 months | |
| Tag | Download | Author | Age | |
| v0.1.1 | commit 11f466e309... | Andreas Grois | 20 months | |
| v0.1.0 | commit 79726a8a66... | Andreas Grois | 20 months | |
| Age | Commit message | Author | Files | Lines |
| 2025-11-30 | Proof that toList has the same length as the heap.HEADmain | Andreas Grois | 1 | -9/+26 |
| 2025-11-16 | Lean 4.25 | Andreas Grois | 2 | -2/+2 |
| 2025-11-16 | Lean 4.24 | Andreas Grois | 1 | -1/+1 |
| 2025-11-16 | Lean 4.23 | Andreas Grois | 7 | -19/+17 |
| 2025-11-15 | Implement Decidable for Nat.isPowerOfTwo and use it. | Andreas Grois | 5 | -115/+91 |
| 2025-11-02 | Lean 4.21 | Andreas Grois | 5 | -30/+31 |
| 2025-10-12 | Lean 4.20.1 | Andreas Grois | 5 | -23/+16 |
| 2025-10-12 | Lean 4.19 | Andreas Grois | 7 | -140/+151 |
| 2025-10-09 | Lean 4.18 | Andreas Grois | 12 | -53/+53 |
| 2025-04-13 | Lean 4.17 | Andreas Grois | 1 | -1/+1 |
| [...] | ||||
| Clone | ||||
| http://git.grois.info/BinaryHeap | ||||
 |
index : BinaryHeap | |
| A toy project about formal validation of a Heap in Lean4 | Andreas Grois |
| aboutsummaryrefslogtreecommitdiff |