How to write SortedMap k (Maybe v) -> SortedMap k v?

Question

Is there an easy way to get from SortedMap k (Maybe v) to SortedMap k v without going to list and back? Nothings should be removed and Justs should be kept.

Answer 1

I do not think so, as SortedMap does not expose its constructors (it is only exporting the top level definition). From the look at the API it seems that converting to a list and back is the way to go.

export
data SortedMap : Type -> Type -> Type where
  Empty : Ord k => SortedMap k v
  M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v