aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Fix wrong index validity check for Nat indices.Andreas Grois2024-08-131-2/+2
* Fix compilation with Lean 4.10.Andreas Grois2024-08-139-102/+92
* heapPopOnlyRemovesRoot is finally doneAndreas Grois2024-08-133-566/+83
* Finish heapRemoveLastWithIndexRelation. That was a piece of work...Andreas Grois2024-08-121-22/+62
* Start heapRemoveLastWithIndexRelationLtAndreas Grois2024-08-121-1/+51
* Continue heapRemoveLastWithIndexRelation.Andreas Grois2024-08-114-6/+19
* Finish heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-112-52/+84
* Continue heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-102-23/+84
* continue heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-101-10/+23
* Continue on heapRemoveLastWithIndexRelationAndreas Grois2024-08-094-12/+40
* First branch of heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-091-5/+19
* heapRemoveLastWithIndexRelation - continuedAndreas Grois2024-08-082-54/+89
* MinorAndreas Grois2024-08-081-0/+6
* Unfinished heapPop proof workAndreas Grois2024-08-082-0/+177
* heapPopReturnsRootAndreas Grois2024-08-044-3/+29
* Update TODOAndreas Grois2024-08-041-19/+9
* heapUpdateRootContainsUpdatedElementAndreas Grois2024-08-041-0/+38
* Finish heapUpdateRootOnlyUpdtesRoot.Andreas Grois2024-08-041-5/+37
* Continue heapUpdateRootOnlyUpdatesRootAndreas Grois2024-08-041-1/+12
* Continue HeapUpdateRootOnlyUpdatesRoot. Left side finished.Andreas Grois2024-08-042-6/+79
* OopsAndreas Grois2024-08-031-0/+48
* Partial proof that HeapUpdateRoot only changes the root.Andreas Grois2024-08-032-1/+2
* Proves about heapRemoveLast.Andreas Grois2024-08-022-3/+93
* Split AdditionalProofs into several files.Andreas Grois2024-08-013-827/+826
* Split HeapProofs into several smaller files.Andreas Grois2024-07-319-687/+702
* Update TODO fileAndreas Grois2024-07-301-6/+3
* Finish heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-301-8/+130
* Minor progress on heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-301-5/+109
* Finish left half of heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-30/+69
* Continue heapRemoveLastWithIndexOnlyRemovesOneElement. Progress!Andreas Grois2024-07-282-28/+19
* Minor, some trial and error.Andreas Grois2024-07-282-8/+59
* 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
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 23:31:58 +0000