[Agda] A different implementation of --without-K

Nils Anders Danielsson nad at cse.gu.se
Fri Nov 29 12:00:26 CET 2013

On 2013-11-28 23:34, Andreas Abel wrote:
> Yes, some of the fail test cases seem only to be there to document
> what *is* rejected.  I do not know what purpose this serves, since I
> would expect only stuff there that *must be* rejected.

The point is that the semantics of --without-K should not be changed by
accident. These examples "must" be rejected until we make a conscious
decision to change the semantics.


More information about the Agda mailing list