--- Day changed Wed Jan 18 2017
drdoWhat's the deal with implicit arguments in constructors?18/01 16:20
drdoIt doesn't seem to be possible to actually use those implicit arguments18/01 16:20
wlesliethe deal?18/01 16:21
drdoApparently it is possible, but even with --show-implicit agda does not show them18/01 16:23
wleslieyou want to pattern match on them?18/01 16:25
wlesliethe argument is a datatype, right, not a function or higher set?18/01 16:26
drdowleslie: The issue was just that they do not appear with agda2-infer-type-maybe-toplevel18/01 16:26
drdoEven with --show-implicit18/01 16:26
wlesliecurious18/01 16:28
wleslieI don't know much about that, will go to sleep now.18/01 16:28
yhhkocan i use reflection with the hott-agda library?18/01 22:10
yhhkoapparently the answer is no because they have overlapping BUILTIN pragmas18/01 22:17
yhhkothat is quite disappointing18/01 22:18
yhhkoapparently you can get some things to work if you write your own Agda.Builtin modules and take out some pragmas18/01 23:51

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