chore: Add empty collection instance to BinomialHeap (#532)

leanprover-community · Jan 16, 2024 · b1ebd72 · b1ebd72
1 parent 01d1cae
commit b1ebd72
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Std/Data/BinomialHeap/Basic.lean b/Std/Data/BinomialHeap/Basic.lean
@@ -502,6 +502,7 @@ variable {α : Type u} {le : α → α → Bool}
 /-- `O(1)`. Make a new empty binomial heap. -/
 @[inline] def empty : BinomialHeap α le := mkBinomialHeap α le
 
+instance : EmptyCollection (BinomialHeap α le) := ⟨.empty⟩
 instance : Inhabited (BinomialHeap α le) := ⟨.empty⟩
 
 /-- `O(1)`. Is the heap empty? -/