[Agda] Feature request: array primitives

[Nils Anders Danielsson]

On 2010-10-19 07:19, Permjacov Evgeniy wrote:
>   Fast arrays may be very interesting, as they may allow rapid correct
> prototyping of numerical software in Agda. Moreover, with use of GPGPU
> bindings they may be of production speed. The rest are some random
> thoughts about how to bring arrays into agda, keeping in ming ghc as
> target language

Is there anything in your list you can't do using the Haskell FFI?

The FFI has one important limitation: Haskell code is not run by the
type-checker.

-- 
/NAD