aboutsummaryrefslogtreecommitdiff
BranchCommit messageAuthorAge
mainProof that toList has the same length as the heap.Andreas Grois5 months
 
TagDownloadAuthorAge
v0.1.1commit 11f466e309...Andreas Grois20 months
v0.1.0commit 79726a8a66...Andreas Grois20 months
 
AgeCommit messageAuthorFilesLines
2024-09-05Add for-loop support and update lean toolchain to 4.11v0.1.1Andreas Grois2-1/+14
2024-08-31Clean up indexOfAuxAddsCurrentIndex slightly.v0.1.0Andreas Grois2-24/+19
2024-08-30First working version of indexOfSomeImpPredTrueAndreas Grois1-3/+107
2024-08-29Continue indexOfSomeImpPredTrueAndreas Grois3-72/+161
2024-08-28Remove redundant contains_iff_index_exists' function.Andreas Grois5-21/+12
2024-08-27Simplify CompleteTree.get, and remove (redundant) CompleteTree.get'Andreas Grois11-421/+251
2024-08-26MinorAndreas Grois1-2/+2
2024-08-26Remove useless proof parameter on CompleteTree.getAndreas Grois14-181/+184
2024-08-25indexOfNoneImpPredFalseAndreas Grois4-4/+70
2024-08-25heapPushRetainsHeapValuesAndreas Grois2-1/+69
[...]
 
Clone
http://git.grois.info/BinaryHeap
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 11:46:24 +0000