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

[Harley D. Eades III]

Hi, everyone.

On Nov 29, 2013, at 5:00 AM, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> 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.

Where is the semantics of --without-K formally written down?

Thanks,
.\ Harley

> 
> -- 
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda