
  0 | module Syntax.IHateParens.SortedMap
  1 | 
  2 | import public Data.SortedMap
  3 | import Data.Vect
  4 | 
  5 | import Syntax.IHateParens.List
  6 | 
  7 | %default total
  8 | 
  9 | public export %inline
 10 | (.asList) : SortedMap k v -> List (k, v)
 11 | m.asList = kvList m
 12 | 
 13 | public export %inline
 14 | (.size) : SortedMap k v -> Nat
 15 | m.size = m.asList.length
 16 | 
 17 | public export %inline
 18 | (.asVect) : (m : SortedMap k v) -> Vect m.size (k, v)
 19 | s.asVect = fromList s.asList
 20 |