[Agda] Re: Builtins

[Jesper Cockx]

On Sat, Apr 25, 2015 at 11:47 PM, Kirill Elagin <kirelagin at gmail.com> wrote:

>
> The funny thing is that, as far as I know, it is not proven that there is
> no other way to derive K, using, maybe, some other weird trick with pattern
> matching. So the `--without-K` is not guaranteed to save you from K, but it
> is believed to do so.
>

In fact, our ICFP '14 paper gives exactly such a guarantee. So if anything
in Agda allows you to prove K with --without-K enabled, it's probably a bug
in the implementation. If you are interested in the subject, you can read
the paper here:
https://lirias.kuleuven.be/bitstream/123456789/452283/2/icfp14-cockxA.pdf

cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150426/d1473b59/attachment.html