aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Lean 4.21HEADmainAndreas Grois39 hours5-30/+31
* Lean 4.20.1Andreas Grois2025-10-125-23/+16
* Lean 4.19Andreas Grois2025-10-127-140/+151
* Lean 4.18Andreas Grois2025-10-0912-53/+53
* Lean 4.17Andreas Grois2025-04-131-1/+1
* Lean 4.16Andreas Grois2025-02-134-11/+14
* Simplify CompleteTree.Internal.heapRemoveLastAux a bitAndreas Grois2025-01-191-18/+11
* Minor, readabilityAndreas Grois2025-01-151-1/+8
* Simplify CompleteTree.heapPush furtherAndreas Grois2025-01-151-30/+32
* MinorAndreas Grois2025-01-131-2/+3
* Minor, just simplify some proofs in CompleteTree.heapPushAndreas Grois2025-01-131-11/+10
* Lean 4.15Andreas Grois2025-01-073-4/+4
* Add BinaryHeap.pushList function.Andreas Grois2024-12-191-1/+9
* Lean 4.14Andreas Grois2024-12-172-2/+1
* Update to Lean 4.13Andreas Grois2024-11-2211-25/+28
* Add a bunch of helper functions. Improve function signatures.Andreas Grois2024-09-149-101/+179
* 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
* 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
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 06:40:49 +0000