Idris2Doc : Data.Array

Data.Array

(source)
Reexports
import public Data.Array.Core
import public Data.Array.Index
import public Data.Array.Indexed
Definitions
fromList : List a -> Array a
  Totality: total
  Visibility: export
fill : Nat -> a -> Array a
  Totality: total
  Visibility: export
generate : (n : Nat) -> (Fin n -> a) -> Array a
  Totality: total
  Visibility: export
iterate : Nat -> (a -> a) -> a -> Array a
  Totality: total
  Visibility: export
force : Array a -> Array a
  Totality: total
  Visibility: export
take : Nat -> Array a -> Array a
  Totality: total
  Visibility: export
drop : Nat -> Array a -> Array a
  Totality: total
  Visibility: export
filter : (a -> Bool) -> Array a -> Array a
  Totality: total
  Visibility: export
mapMaybe : (a -> Maybe b) -> Array a -> Array b
  Totality: total
  Visibility: export