Idris2Doc : Data.Linear.Array

Data.Linear.Array

Array : (Type -> Type) -> Type
Parameters: arr
Methods:
read : (1 _ : arrt) -> Int -> Maybet
size : (1 _ : arrt) -> Int

Implementations:
ArrayLinArray
ArrayIArray
IArray : Type -> Type
Totality: total
Constructor: 
MkIArray : IOArrayt -> IArrayt
LinArray : Type -> Type
Totality: total
Constructor: 
MkLinArray : IOArrayt -> LinArrayt
MArray : (Type -> Type) -> Type
Parameters: arr
Constraints: Array arr
Methods:
newArray : (size : Int) -> (1 _ : ((1 _ : arrt) -> a)) -> a
write : (1 _ : arrt) -> Int -> t -> arrt
mread : (1 _ : arrt) -> Int -> Res (Maybet) (const (arrt))
msize : (1 _ : arrt) -> Res Int (const (arrt))

Implementation: 
MArrayLinArray
copyArray : MArrayarr => Int -> (1 _ : arrt) -> LPair (arrt) (arrt)
mread : MArrayarr => (1 _ : arrt) -> Int -> Res (Maybet) (const (arrt))
msize : MArrayarr => (1 _ : arrt) -> Res Int (const (arrt))
newArray : MArrayarr => Int -> (1 _ : ((1 _ : arrt) -> a)) -> a
read : Arrayarr => (1 _ : arrt) -> Int -> Maybet
size : Arrayarr => (1 _ : arrt) -> Int
toIArray : (1 _ : LinArrayt) -> (IArrayt -> a) -> a
write : MArrayarr => (1 _ : arrt) -> Int -> t -> arrt