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

--- Day changed Wed Jan 11 2017
apostolisI am still in the blind with regards to Sized types.11/01 09:27
apostolisI noticed that adding (with a constructor) two types where the first has Size i and the other j : Size< i does not result in an error when the outcome is Size j.11/01 09:29
apostolisSo any type that is observable i times, can also be observable less times which makes sense.11/01 09:31
apostolisBut now, I am in a similar position and the type checker rejects the code.11/01 09:33
redfish64drdo: I like http://people.inf.elte.hu/divip/AgdaTutorial/Index.html11/01 09:37
redfish64It has a lot of exercises where you build structures just like std-lib, then in future chapters, you use std-lib in lieu of the structures you built11/01 09:38
apostolisSince the sizes are in the values of the dependent type, and the object itself is finite, I use a function to manually reconstruct the object to reduce their Size but this seems like a waste.11/01 09:39
pgiarrussoquestion: anybody knows whether typed deBrujin indexes work —without-K?11/01 10:06
effectfu1pgiarrusso: like this? https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/SysF/Syntax.agda11/01 10:21
pgiarrussoeffectfu1: those are well-scoped, but that looks interesting!11/01 10:22
pgiarrussoI guess that relies on Jesper Cockx clever K-less pattern matching?11/01 10:23
effectfu1pgiarrusso: I don't know, it's not mine11/01 10:23
pgiarrussoI realize :-)11/01 10:23
effectfu1aren't these indices? https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/SysF/Syntax.agda#L22511/01 10:23
drdoredfish64: Thanks, I'll check it out11/01 20:28

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