/home/laney/.irssi/irclogs/Freenode/#agda.log-20170114

--- Day changed Fri Jan 13 2017
rgrinbergIs there any way to load these README modules from  the stdlib? README.Record for example13/01 03:19
apostolisHas anyone had problems with Sized types and "with" when you have subtypes?13/01 10:34
effectfu1apostolis: everyone has always problems with Sized types and anything else13/01 10:35
apostolisConsider this : {i : Size} {j : Size< i} {k : Size< j}13/01 10:37
apostolisThe type of k is also {k : Size< i}13/01 10:37
apostolisI am in the investigation face but maybe agda is confused by that.13/01 10:38
mietekapostolis: lots of problems with Sized types13/01 10:55
mietekapostolis: "Unfortunately, the handling of size-max is not well-developed in Agda yet." — not sure if that applies there13/01 10:55
apostolismietek : After Abel provides some general guidelines how to use Sized types, I will probably start looking at the issues in github.13/01 12:50
mietekapostolis: do you mean you’re working with Abel to improve Agda?13/01 12:54
apostolisNp : I hope he writes a tutorial.13/01 12:55
apostolisNo13/01 12:55
apostolisI will look at the issues to see where agda fails with sized types.13/01 12:56
yhhkocan anyone tell me why this usage of instance arguments of function type doesn't work? http://lpaste.net/35118013/01 15:33
yhhkoor if this would be a bug?13/01 15:37

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