Idris2Doc : Data.Linear.Array

Data.Linear.Array

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
data IArray : Type -> Type
  Totality: total
  Constructor: 
MkIArray : IOArray t -> IArray t
data LinArray : Type -> Type
  Totality: total
  Constructor: 
MkLinArray : IOArray t -> LinArray t
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
copyArray : MArray arr => Int -> (1 _ : arr t) -> LPair (arr t) (arr t)
  
mread : MArray arr => (1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))
  
msize : MArray arr => (1 _ : arr t) -> Res Int (const (arr t))
  
newArray : MArray arr => Int -> (1 _ : ((1 _ : arr t) -> a)) -> a
  
read : Array arr => (1 _ : arr t) -> Int -> Maybe t
  
size : Array arr => (1 _ : arr t) -> Int
  
toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
  
write : MArray arr => (1 _ : arr t) -> Int -> t -> Res Bool (const (arr t))