<br><div class="gmail_quote">On Sun, Nov 1, 2009 at 9:57 AM, Julian Beaumont <span dir="ltr"><<a href="mailto:jp.beaumont@student.qut.edu.au">jp.beaumont@student.qut.edu.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hey Ruben,<br>
<br>
In the definition<br>
<div class="im"><br>
exPrimes : ∃ Prime<br>
exPrimes = 2 , 2-prime<br>
<br>
</div>agda applies 2-prime to implicit arguments before trying to typecheck<br>
it, so you end up with something equivalent to<br>
<br>
exPrimes : ∃ Prime<br>
exPrimes = 2 , (2-prime {_})<br>
<br>
You can see now that (2-prime {_}) doesn't have type Prime 2, hence<br>
the error message. To get around this you need to do something like<br>
<br>
exPrimes : ∃ Prime<br>
exPrimes = 2 , (λ {_} → 2-prime)<font color="#888888"><br></font></blockquote><div><br>Indeed. Alternatively change the definition of Prime making the i explicit.<br><br>/ Ulf <br></div></div><br>