aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Add for-loop support and update lean toolchain to 4.11v0.1.1Andreas Grois2024-09-052-1/+14
|
* 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
| | | | Case for index equal removed index.
* Finish heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-112-52/+84
| | | | | | and optimize it a bit. All that omega and simp was really increasing compilation time... So, a lot of smaller proofs in that function are now done by hand instead.
* 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
| | | | | It could use some cleanup though. Compiling it takes quite long already...
* 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
|
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 16:48:02 +0000