<div dir="ltr"><div>Actually, that paper is outdated as well. Specifically, it now uses a new more powerful unification algorithm as described in our papers "Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data" (<a href="https://lirias.kuleuven.be/handle/123456789/544210">https://lirias.kuleuven.be/handle/123456789/544210</a>) and "Lifting Proof-Relevant Unification to Higher Dimensions" (<a href="https://lirias.kuleuven.be/handle/123456789/556894">https://lirias.kuleuven.be/handle/123456789/556894</a>). I didn't realize we still use the documentation of the original --without-K, I'll update it as soon as possible.<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 30, 2017 at 6:09 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 2017-03-30 16:35, Andrés Sicard-Ramírez wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
See <a href="http://agda.readthedocs.io/en/latest/language/without-k.html" rel="noreferrer" target="_blank">http://agda.readthedocs.io/en/<wbr>latest/language/without-k.html</a> .<br>
</blockquote>
<br>
This documentation is outdated. There is a new implementation of<br>
--without-K now, see Eliminating dependent pattern matching without K by<br>
Cockx et al. (<a href="https://doi.org/10.1017/S0956796816000174" rel="noreferrer" target="_blank">https://doi.org/10.1017/S0956<wbr>796816000174</a>).<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD</font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>