[Agda] bug in definitions using "_"?

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Dec 19 17:58:55 CET 2013

On 19/12/13 16:17, Jesper Cockx wrote:
> This is indeed fixed in the development version: see
> http://code.google.com/p/agda/issues/detail?id=920.

Interesting. But in the example I gave (in Agda, when the
hypotheses are replaced by postulates I do get yellow (as I should),
indicating that unification works differently for postulates
(correctly!) before the fix in the development version.


More information about the Agda mailing list