aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
...
* Continue heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-11/+35
| | | | One of 4 branches done.
* 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
| | | | This is a preparation step for additional proofs.
* 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
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 19:50:55 +0000