Idris2Doc : Data.HashMap.SparseArray

Data.HashMap.SparseArray

(source)
Reexports
import public Data.HashMap.Array
Definitions
record SparseArray : Type -> Type
  An array storing up to 64 elements

  Totality: total
  Visibility: public export
  Constructor: 
MkSparseArray : Bits64 -> Array a -> SparseArray a

  Projections:
  
.array : SparseArray a -> Array a
  
.bitmap : SparseArray a -> Bits64

  Hints:
  
Eq a => Eq (SparseArray a)
  
Foldable SparseArray
  
Functor SparseArray
  
Show a => Show (SparseArray a)
.bitmap : SparseArray a -> Bits64
  Totality: total
  Visibility: public export
bitmap : SparseArray a -> Bits64
  Totality: total
  Visibility: public export
.array : SparseArray a -> Array a
  Totality: total
  Visibility: public export
array : SparseArray a -> Array a
  Totality: total
  Visibility: public export
empty : SparseArray a
  Totality: total
  Visibility: export
singleton : (Bits32, a) -> SparseArray a
  Totality: total
  Visibility: export
doubleton : (Bits32, a) -> (Bits32, a) -> SparseArray a
  Totality: total
  Visibility: export
fromList : List (Bits32, a) -> SparseArray a
  Totality: total
  Visibility: export
hasEntry : Bits32 -> SparseArray a -> Bool
  Totality: total
  Visibility: export
findIndex : Bits32 -> Bits64 -> Bits32
  Totality: total
  Visibility: export
index : Bits32 -> SparseArray a -> Maybe a
  Totality: total
  Visibility: export
set : Bits32 -> a -> SparseArray a -> SparseArray a
  Totality: total
  Visibility: export
delete : Bits32 -> SparseArray a -> SparseArray a
  Totality: total
  Visibility: export
length : SparseArray a -> Nat
  Totality: total
  Visibility: export
indexes : SparseArray a -> List Bits32
  Totality: total
  Visibility: export
toList : SparseArray a -> List (Bits32, a)
  Totality: total
  Visibility: export