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

[Andreas Abel]

On 29.11.2013 18:11, Harley D. Eades III wrote:
> 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?

There is not much written.  The documentation of the --without-K 
variants is in the respective release notes.

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/