[Agda] primes

[Ulf Norell]

On Sun, Nov 1, 2009 at 9:57 AM, Julian Beaumont <
jp.beaumont at student.qut.edu.au> wrote:

> Hey Ruben,
>
> In the definition
>
> exPrimes : ∃ Prime
> exPrimes = 2 , 2-prime
>
> agda applies 2-prime to implicit arguments before trying to typecheck
> it, so you end up with something equivalent to
>
> exPrimes : ∃ Prime
> exPrimes = 2 , (2-prime {_})
>
> You can see now that (2-prime {_}) doesn't have type Prime 2, hence
> the error message. To get around this you need to do something like
>
> exPrimes : ∃ Prime
> exPrimes = 2 , (λ {_} → 2-prime)
>

Indeed. Alternatively change the definition of Prime making the i explicit.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091101/d38cc270/attachment.html