--- Day changed Sun Jan 21 2018
trikl[m]What do the double dots before an implicit argument mean?21/01 22:54
pgiarrussotrikl[m]: *double* dots? as in `..`? never seen that... got a sample agda file?21/01 23:16
trikl[m]https://github.com/UlfNorell/agda-prelude/blob/master/src/Prelude/Vec.agda#L9621/01 23:17
trikl[m]It's part of https://agda.readthedocs.io/en/v2.5.3/language/lexical-structure.html but I can't find any further mention to it21/01 23:18
pgiarrussoUlf Norell says “runtime irrelevance” whatever that means: https://github.com/UlfNorell/agda-prelude/commit/701c1b4a85c495097cb39e0bd9005dbf60dfa05e#diff-e27a568aa2737d59bbf3cdb08e75815d21/01 23:19
pgiarrussoI know Agda has single dot for irrelevance, wondering how “runtime irrelevance” is different21/01 23:19
pgiarrussohave you already checked Agda’s CHANGELOG?21/01 23:20
pgiarrussothat used to be the only accurate documentation for Agda21/01 23:20
pgiarrussoand I guess the feature is recent enough it should be there21/01 23:20
trikl[m]Oh I will look at that, thanks21/01 23:21
pgiarrussomaybe we should link to the CHANGELOG in the topic or the manual or...21/01 23:23
pgiarrussoand while I’m sharing tricks: I was so confused by the code that I reached immediately for the git history21/01 23:25
pgiarrusso(though I have also used Agda for long enough without ever seeing double dots that I could guess it’s a new feature)21/01 23:26
trikl[m]I should have thought of that :)21/01 23:29
trikl[m]I don't think it's mentioned in the CHANGELOG though21/01 23:31

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