[Agda] lists/vectors

Nils Anders Danielsson nad at chalmers.se
Mon Oct 15 13:04:50 CEST 2012

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)


More information about the Agda mailing list