aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Clean up indexOfAuxAddsCurrentIndex slightly.v0.1.0Andreas Grois2024-08-312-24/+19
* First working version of indexOfSomeImpPredTrueAndreas Grois2024-08-301-3/+107
* Continue indexOfSomeImpPredTrueAndreas Grois2024-08-293-72/+161
* Remove redundant contains_iff_index_exists' function.Andreas Grois2024-08-285-21/+12
* Simplify CompleteTree.get, and remove (redundant) CompleteTree.get'Andreas Grois2024-08-2711-421/+251
* MinorAndreas Grois2024-08-261-2/+2
* Remove useless proof parameter on CompleteTree.getAndreas Grois2024-08-2614-181/+184
* indexOfNoneImpPredFalseAndreas Grois2024-08-254-4/+70
* heapPushRetainsHeapValuesAndreas Grois2024-08-252-1/+69
* heapPushContainsValueAndreas Grois2024-08-223-1/+49
* heapRemoveAtOnlyRemovesAtAndreas Grois2024-08-222-1/+62
* Minor: Remove tactics mode for Nat.ble adaptersAndreas Grois2024-08-211-10/+9
* Minor: Update TODOAndreas Grois2024-08-201-1/+1
* heapRemoveAtReturnsElementAtAndreas Grois2024-08-202-0/+30
* heapUpdateAtOnlyUpdatesAtAndreas Grois2024-08-194-5/+167
* heapUpdateAtReturnsElementAtAndreas Grois2024-08-192-0/+44
* Update TODOAndreas Grois2024-08-151-0/+4
* Minor: Add some commentsAndreas Grois2024-08-153-1/+28
* 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
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 12:13:07 +0000