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