Idris2Doc : Syntax.IHateParens.SortedMap.Dependent

Syntax.IHateParens.SortedMap.Dependent

(source)
Reexports
import public Data.SortedMap.Dependent
Definitions
.asList : SortedDMap k v -> List (x : k ** v x)
  Totality: total
  Visibility: public export
.size : SortedDMap k v -> Nat
  Totality: total
  Visibility: public export
.asVect : (m : SortedDMap k v) -> Vect (m .size) (x : k ** v x)
  Totality: total
  Visibility: public export