diff options
| author | Andreas Grois <andi@grois.info> | 2024-01-13 15:21:39 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-01-13 15:21:39 +0100 |
| commit | 25f2f5c2ba05433ad07cf855b8a61ab199107cee (patch) | |
| tree | 4faa9973dcf49bd1bb23bd1f398f279863082d35 /Day7.lean | |
| parent | e6facae131c5b294904e60a9108300f11c4ebfb9 (diff) | |
Fix Heap Insert preserves Heap Proof. Preconditions were wrong.
And with wrong I mean "unfulfillable if any elements in the heap should
be equal to each other".
I'm still not fully happy with this, as it relies on lt being compatible
with Eq, but yeah, it works for now.
Diffstat (limited to 'Day7.lean')
0 files changed, 0 insertions, 0 deletions