From 06f554b94d0be4d08720e3988b40a0152d483538 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Sep 2021 15:59:35 -0700 Subject: [PATCH] feat: add `RBTree.toArray` --- src/Std/Data/RBTree.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean index ef5cfde3d5..3d5ff8ca81 100644 --- a/src/Std/Data/RBTree.lean +++ b/src/Std/Data/RBTree.lean @@ -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