[Agda] bug in definitions using "_"?

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Dec 19 12:00:12 CET 2013



On 19/12/13 10:37, Ulf Norell wrote:
> It looks like this has been fixed. In the development version I get
> yellow on all variants of the example.

Great. Fortunately I don't use "_" often in proofs. But I worry that
the one or two occasions in which I did may be unfillable!

I shall try the development version.

Thanks,
Martin


More information about the Agda mailing list