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

Andreas Abel andreas.abel at ifi.lmu.de
Fri Nov 29 18:36:53 CET 2013

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.


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

More information about the Agda mailing list