feat: add RBTree.toArray

This commit is contained in:
Leonardo de Moura 2021-09-17 15:59:35 -07:00
parent da69b10056
commit 06f554b94d

View file

@ -52,6 +52,9 @@ instance : ForIn m (RBTree α cmp) α where
@[specialize] def toList (t : RBTree α cmp) : List α :=
t.revFold (fun as a => a::as) []
@[specialize] def toArray (t : RBTree α cmp) : Array α :=
t.fold (fun as a => as.push a) #[]
@[inline] protected def min (t : RBTree α cmp) : Option α :=
match RBMap.min t with
| some ⟨a, _⟩ => some a