ddc-code-0.4.2.1: tetra/base/Data/Array.ds

module Data.Array
export { allocArray; readArray; writeArray }

import foreign boxed type
 Array : Region ~> Data ~> Data

import foreign c value
 allocArray : [r: Region]. [a: Data]. Nat# -> a -> S (Alloc r) (Array r a)
 readArray  : [r: Region]. [a: Data]. Array r a -> Nat# -> S (Read r) a
 writeArray : [r: Region]. [a: Data]. Array r a -> Nat# -> a -> S (Write r) Void#