diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-11 19:10:46 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-11 19:10:46 +0200 |
| commit | 0086a3de4a8cc0f6c6390bcb951e0c7fb65d9034 (patch) | |
| tree | 80f8a8b299576828ecb89680e6ea888247de12d7 /BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | |
| parent | 50a68bfb858b0251005252f82f3d806fd3c78cba (diff) | |
Finish heapRemoveLastWithIndexRelationGt
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.
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean')
0 files changed, 0 insertions, 0 deletions