aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
* Continue heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-11/+35
* Continue on heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-22/+53
* Progress?Andreas Grois2024-07-271-3/+34
* Continue heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-272-14/+109
* Partial implementation of heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-265-12/+79
* Finish contains_iff_index_existsAndreas Grois2024-07-252-10/+92
* Start contains_iff_index_exists implementation. Unfinished.Andreas Grois2024-07-246-35/+190
* Fix performance issue in CompleteTree.contains.Andreas Grois2024-07-241-6/+7
* Minor: Fix indentation. Sorry.Andreas Grois2024-07-241-12/+12
* Add CompleteTree.contains. Decidable Predicate.Andreas Grois2024-07-241-0/+28
* Add CompleteTree/AdditionalOperations.lean for non-heap operations.Andreas Grois2024-07-234-48/+53
* Split code in multiple source files. Separate proofs and logic.Andreas Grois2024-07-239-1148/+1220
* Add GetElem instances.Andreas Grois2024-07-222-14/+43
* Initial commit.Andreas Grois2024-07-2211-0/+1543