| Branch | Commit message | Author | Age | |
|---|---|---|---|---|
| main | Lean 4.21 | Andreas Grois | 45 hours | |
| Tag | Download | Author | Age | |
| v0.1.1 | commit 11f466e309... | Andreas Grois | 14 months | |
| v0.1.0 | commit 79726a8a66... | Andreas Grois | 14 months | |
| Age | Commit message | Author | Files | Lines |
| 2024-09-05 | Add for-loop support and update lean toolchain to 4.11v0.1.1 | Andreas Grois | 2 | -1/+14 |
| 2024-08-31 | Clean up indexOfAuxAddsCurrentIndex slightly.v0.1.0 | Andreas Grois | 2 | -24/+19 |
| 2024-08-30 | First working version of indexOfSomeImpPredTrue | Andreas Grois | 1 | -3/+107 |
| 2024-08-29 | Continue indexOfSomeImpPredTrue | Andreas Grois | 3 | -72/+161 |
| 2024-08-28 | Remove redundant contains_iff_index_exists' function. | Andreas Grois | 5 | -21/+12 |
| 2024-08-27 | Simplify CompleteTree.get, and remove (redundant) CompleteTree.get' | Andreas Grois | 11 | -421/+251 |
| 2024-08-26 | Minor | Andreas Grois | 1 | -2/+2 |
| 2024-08-26 | Remove useless proof parameter on CompleteTree.get | Andreas Grois | 14 | -181/+184 |
| 2024-08-25 | indexOfNoneImpPredFalse | Andreas Grois | 4 | -4/+70 |
| 2024-08-25 | heapPushRetainsHeapValues | Andreas Grois | 2 | -1/+69 |
| [...] | ||||
| Clone | ||||
| http://git.grois.info/BinaryHeap | ||||
 |
index : BinaryHeap | |
| A toy project about formal validation of a Heap in Lean4 | Andreas Grois |
| aboutsummaryrefslogtreecommitdiff |