[Agda] refl and pattern matching
andres.sicard.ramirez at gmail.com
Sat Apr 6 20:03:08 CEST 2013
In http://thread.gmane.org/gmane.comp.lang.agda/4971/focus=4980 Martin
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) ?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda