[Agda] lists/vectors

[Nils Anders Danielsson]

On 2012-10-14 02:45, Amr Sabry wrote:
> 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.

One alternative is to do the checking on the Agda side:

   List Bool → Maybe (Vec Bool 32)

-- 
/NAD