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