BinaryHeap/TODO, branch v0.1.0 A toy project about formal validation of a Heap in Lean4 https://git.grois.info/BinaryHeap/atom/TODO?h=v0.1.0 2024-08-30T22:05:44Z Clean up indexOfAuxAddsCurrentIndex slightly. 2024-08-30T22:05:44Z Andreas Grois andi@grois.info 2024-08-30T22:05:44Z urn:sha1:79726a8a669ff879db4ae14b8e27af357dd7c7b7 indexOfNoneImpPredFalse 2024-08-25T20:48:10Z Andreas Grois andi@grois.info 2024-08-25T20:48:10Z urn:sha1:e47e4b79142bcee5bcdc4647dc71c7ce3954cf0b heapPushRetainsHeapValues 2024-08-24T22:14:57Z Andreas Grois andi@grois.info 2024-08-24T21:30:10Z urn:sha1:a067c3ad82441726543b739e4b57b9a3018f9416 heapPushContainsValue 2024-08-22T21:26:17Z Andreas Grois andi@grois.info 2024-08-22T21:26:17Z urn:sha1:e58783388fb83a0b53075855955a99f947ee0f7d heapRemoveAtOnlyRemovesAt 2024-08-21T22:01:00Z Andreas Grois andi@grois.info 2024-08-21T22:01:00Z urn:sha1:737026d6c1563febe4f8c974d273f77b3209a569 Minor: Update TODO 2024-08-20T21:53:35Z Andreas Grois andi@grois.info 2024-08-20T21:53:35Z urn:sha1:6cb35171621051aec03906656ffa266f5947380d heapUpdateAtOnlyUpdatesAt 2024-08-19T20:45:41Z Andreas Grois andi@grois.info 2024-08-19T20:45:41Z urn:sha1:7d5df252a6e885f8b1ffab49196e0a4cc4b0131a Update TODO 2024-08-15T18:35:23Z Andreas Grois andi@grois.info 2024-08-15T18:35:23Z urn:sha1:d9690a03ac14baa0f9c4dc72144438a61f905a78 heapPopOnlyRemovesRoot is finally done 2024-08-12T22:11:11Z Andreas Grois andi@grois.info 2024-08-12T22:11:11Z urn:sha1:4f9585b8617ecb65fb97408b831ff45ef25ad0c3 heapPopReturnsRoot 2024-08-04T19:57:44Z Andreas Grois andi@grois.info 2024-08-04T19:57:44Z urn:sha1:824f6328a847805fdc6fd89d9c447824fa5e36e6