refactor: implement `BinaryHeap` using `Vector`

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

242 stars 101 forks source link

Open fgdorais opened 4 months ago

fgdorais commented 4 months ago

This is a follow-up to #849 which uses #793 to simplify major parts of the code, paving the way toward correctness proofs for BinaryHeap.

leanprover-community-bot commented 2 weeks ago

Mathlib CI status (docs):

🟡 Mathlib branch batteries-pr-testing-850 build against this PR was cancelled. (2024-10-01 06:45:20) View Log
❌ Mathlib branch batteries-pr-testing-850 built against this PR, but the archive failed. (2024-10-01 07:40:03) View Log
✅ Mathlib branch batteries-pr-testing-850 has successfully built against this PR. (2024-10-01 12:54:16) View Log