Data.Linear.Array

Definitions

interface Array : (Type -> Type) -> Type

Parameters: arr
Methods:

read : (1 _ : arr t) -> Int -> Maybe t

size : (1 _ : arr t) -> Int

Implementations:

Array LinArray

Array IArray

read : Array arr => (1 _ : arr t) -> Int -> Maybe t

Visibility: public export

size : Array arr => (1 _ : arr t) -> Int

Visibility: public export

interface MArray : (Type -> Type) -> Type

Parameters: arr
Constraints: Array arr
Methods:

newArray : Int -> (1 _ : ((1 _ : arr t) -> a)) -> a

write : (1 _ : arr t) -> Int -> t -> Res Bool (const (arr t))

mread : (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))

msize : (1 _ : arr t) -> Res Int (const (arr t))

Implementation: 

MArray LinArray

newArray : MArray arr => Int -> (1 _ : ((1 _ : arr t) -> a)) -> a

Visibility: public export

write : MArray arr => (1 _ : arr t) -> Int -> t -> Res Bool (const (arr t))

Visibility: public export

mread : MArray arr => (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))

Visibility: public export

msize : MArray arr => (1 _ : arr t) -> Res Int (const (arr t))

Visibility: public export

data IArray : Type -> Type

Totality: total
Visibility: export
Constructor: 

MkIArray : IOArray t -> IArray t

Hint: 

Array IArray

data LinArray : Type -> Type

Totality: total
Visibility: export
Constructor: 

MkLinArray : IOArray t -> LinArray t

Hints:

Array LinArray

MArray LinArray

toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a

Visibility: export

copyArray : MArray arr => Int -> (1 _ : arr t) -> LPair (arr t) (arr t)

Visibility: export