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