[Agda] refl and pattern matching

[Andrés Sicard-Ramírez]

Hi,

In http://thread.gmane.org/gmane.comp.lang.agda/4971/focus=4980 Martin
Escardo wrote:

In fact, I would like to hear from the Agda developers and advisors how
> close or far Agda is from the MLTT family of type theories.
>
> ...
>
> (1) Pattern matching.
>
>      Is fine provided refl is not a pattern (except for the definition
>      of J).  Good to have without-K, but not so good that there isn't a
>      theory of pattern matching without K, or any assurance that
>      without-K actually works. This is particularly relevant for the
>      HoTT enthusiasts using Agda.
>

Assuming that the option --without-K works, why I cannot use refl in
pattern matching (except for the definition of J) ?

Thanks,

--
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130406/1c13e7cf/attachment.html