--- Day changed Wed Jun 28 2017
rntzdoes agda have copattern synonyms the same way it has pattern synonyms?28/06 20:23
gallais_Not that I know of. Sounds like a feature request! https://github.com/agda/agda/issues28/06 20:29
{AS}rntz: could you give an example? 28/06 20:38
{AS}(I don't think it has, but it would be nice to know the usecase)28/06 20:39
gallais_pattern π₁ t = proj₁ t28/06 20:41
gallais_pattern π₂ t = proj₁ (proj₂ t)28/06 20:41
gallais_pattern π₃ t = proj₁ (proj₂ (proj₂ t))28/06 20:41
gallais_etc.28/06 20:41
{AS}I see, makes sense28/06 20:55
rntzyeah, like that.28/06 21:04
rntzissue submitted: https://github.com/agda/agda/issues/262228/06 23:25

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!