[Agda] lists/vectors

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Mon Oct 15 08:30:40 CEST 2012

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


More information about the Agda mailing list