[Agda] Agda options

[Jesper Cockx]

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" (
https://lirias.kuleuven.be/handle/123456789/544210) and "Lifting
Proof-Relevant Unification to Higher Dimensions" (
https://lirias.kuleuven.be/handle/123456789/556894). I didn't realize we
still use the documentation of the original --without-K, I'll update it as
soon as possible.

-- Jesper

On Thu, Mar 30, 2017 at 6:09 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2017-03-30 16:35, Andrés Sicard-Ramírez wrote:
>
>> See http://agda.readthedocs.io/en/latest/language/without-k.html .
>>
>
> This documentation is outdated. There is a new implementation of
> --without-K now, see Eliminating dependent pattern matching without K by
> Cockx et al. (https://doi.org/10.1017/S0956796816000174).
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170330/ddc1bc7d/attachment-0001.html>