[Agda] lists/vectors

[Andrés Sicard-Ramírez]

On Sat, Oct 13, 2012 at 7:45 PM, Amr Sabry <sabry at cs.indiana.edu> wrote:
> Hi all,
>
> Probably a fairly basic question...
>
> Say I have an Agda module that works with things of type
>
>   Vector Bool 32
>
> How does one write a complete program, i.e., an external Haskell
> wrapper, that interacts with this module? I am thinking of a Haskell
> wrapper that reads an arbitrary string, checks that the string length is
> 32, and if so calls the Agda code. This approach requires some
> function:
>
>   (xs : List Bool) -> Vector Bool 32

I guess you can use the function fromList
http://www.cse.chalmers.se/~nad/listings/lib-0.6/Data.Vec.html#4403
instead.

-- 
Andrés