search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

feat: add `BinaryHeap` #849

Closed fgdorais closed 2 months ago

fgdorais commented 2 months ago

Moved from Mathlib with minimal adaptations.

fgdorais commented 2 months ago

I moved to the Batteries namespace. That can be reverted if necessary.

This can be merged as-is right now. Soon, I will update some parts to use Vector which will hopefully simplify adding the missing correctness proofs. But that can wait in the interest of decluttering Mathlib.