Data.DArray

Reexports

Definitions

record DArray : (i : Type) -> (i -> Type) -> Type

Totality: total
Visibility: export
Constructor: 

DA : AnyPtr -> DArray i p

Projection: 

.arr : DArray i p -> AnyPtr

at : Enum i n => DArray i p -> (x : i) -> (x `p`)

Totality: total
Visibility: export

record MDArray : Type -> (i : Type) -> (i -> Type) -> Type

Totality: total
Visibility: export
Constructor: 

MDA : AnyPtr -> MDArray s i p

Projection: 

.arr : MDArray s i p -> AnyPtr

dget : Enum i n => MDArray s i p -> (x : i) -> F1 s ((x `p`))

Totality: total
Visibility: export

dset : Enum i n => MDArray s i p -> (x : i) -> (x `p`) -> F1' s

Totality: total
Visibility: export

unsafeFreeze : MDArray s i p -> F1 s (DArray i p)

Totality: total
Visibility: export

freeze : Enum i n => MDArray s i p -> F1 s (DArray i p)

Totality: total
Visibility: export

unsafeMDArray1 : (0 i : Type) -> (0 p : (i -> Type)) -> Enum i n => F1 s (MDArray s i p)

Totality: total
Visibility: export

mdarrayAll1 : (0 i : Type) -> (0 p : (i -> Type)) -> {auto enum : Enum i n} -> All p values -> F1 s (MDArray s i p)

  A safe constructor for mutable dependent arrays.

Totality: total
Visibility: export

mdarrayAuto1 : (0 i : Type) -> (0 p : (i -> Type)) -> {auto enum : Enum i n} -> All p values => F1 s (MDArray s i p)

  Like `mdarrayAll1` but accepts the list of values as an auto implicit.

Totality: total
Visibility: export

mdarray1 : (0 i : Type) -> (0 p : (i -> Type)) -> Enum i n => ((v : i) -> (v `p`)) -> F1 s (MDArray s i p)

  A safe constructor for mutable dependent arrays.

Totality: total
Visibility: export

darray : (0 i : Type) -> (0 p : (i -> Type)) -> Enum i n => ((v : i) -> (v `p`)) -> DArray i p

Totality: total
Visibility: export

darrayAll : (0 i : Type) -> (0 p : (i -> Type)) -> {auto enum : Enum i n} -> All p values -> DArray i p

Totality: total
Visibility: export

darrayAuto : (0 i : Type) -> (0 p : (i -> Type)) -> {auto enum : Enum i n} -> All p values => DArray i p

Totality: total
Visibility: export