<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Sat, Apr 25, 2015 at 11:47 PM, Kirill Elagin <span dir="ltr">&lt;<a href="mailto:kirelagin@gmail.com" target="_blank">kirelagin@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span class=""></span><br><div class="gmail_quote"><div>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.<br></div></div></div></blockquote><br></div><div class="gmail_quote">In fact, our ICFP &#39;14 paper gives exactly such a guarantee. So if anything in Agda allows you to prove K with --without-K enabled, it&#39;s probably a bug in the implementation. If you are interested in the subject, you can read the paper here: <a href="https://lirias.kuleuven.be/bitstream/123456789/452283/2/icfp14-cockxA.pdf">https://lirias.kuleuven.be/bitstream/123456789/452283/2/icfp14-cockxA.pdf</a><br><br></div><div class="gmail_quote">cheers,<br></div><div class="gmail_quote">Jesper<br></div><br></div></div>