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

--- Day changed Thu Aug 17 2017
kclancyIt seems that the semantics for the inf size has changed since the original paper. It used to be the size of  data "without known height bound". The language reference now says that is a size larger than the size of any data one could possibly define in Agda, which is quite different.17/08 00:26
kclancyOkay, the old notion of inf offers no expressive power over wrapping a constructor in a size abstraction. Putting size abstractions everywhere might be cumbersome, but now I think that I understand what my options are when working with sized types.17/08 00:37
kclancyHere is what I actually wanted: https://paste.ofcode.org/MzMRcXx9bbmN6T7muq5tVQ17/08 01:22
kclancyBut I'm worried that if I continue using sized types that everything will be wrapped in size abstractions and that it will end up obfuscating the program.17/08 01:23
Saizankclancy: the way that the "without known height bound" works, is that Agda will figure out some subtyping rules so that T {i} is a subtype of T {inf}, but it will do so _after_ you completed the definition of T itself17/08 09:13
Saizankclancy: so they are not yet available for TFormal there17/08 09:14
Saizankclancy: this might be improved in the future, tbh17/08 09:15
Saizankclancy: an option would also be to write your own conversion function T {i17/08 09:16
SaizanT {i} -> T {\inf}17/08 09:16
Saizanmutually with the definition of T17/08 09:16
Saizannot sure if that's better though.17/08 09:16
zaoqiHow do I implement a language like agda?17/08 10:28
kclancySaizan: the definition of the converter function produces an i != inf error.17/08 12:59
kclancyOther forms of size subtyping work, though. Are you sure that the intended semantics of inf haven't been changed?17/08 13:02
kclancyNo wait. Finite to inf subtyping works as long as the definition of after the definition of any definition that I'd mutually recursive with T.17/08 13:04
kclancyI meant to type "as long as the definition Intensity Intensity is after"17/08 13:06
kclancyThat is not what I meant to type at all. Sorry, this is cell phone auto-correct's fault. " as long as the definition is after."17/08 13:08
Saizankclancy: yeah, it does compute the subtyping information after the mutual block is checked17/08 13:10
Saizankclancy: a converter function is usually possible, defined by recursion, but i would have to see the code17/08 13:11
marchdownhello17/08 13:24
marchdownI'm trying to set the standard library and I'm getting a parse error on Data/Empty.agda when I try to typecheck my buffer. Is that supposed to happen?17/08 13:29
marchdown^ set up17/08 13:29
kevin_Saizan: This is kclancy. Here is my attempt to use a converter function: https://paste.ofcode.org/E4wNr9i4WCLZeJENMrwDLN17/08 13:43
Saizanmarchdown: make sure your version of agda matches your version of the stdlib17/08 13:52
Saizankclancy: conv needs to actually pattern match on Tâ‚€ and recurse17/08 15:03
stellegI'm trying to follow the guidelines at http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda for getting unicode working, but not having any luck. I'm getting the warning that inputenc package ignored with utf8 based engines. Anyone familiar with this issue?17/08 15:10
Saizanstelleg: see the "{xe|lua}latex and proper unicode fonts" section if you are using one of those17/08 15:12
kclancyOh, I see. That sounds like a pain. I will just wrap environment constructors in size abstractions instead.17/08 15:21
stellegSaizan: thanks. I've been trying xelatex and laulatex due to getting errors like "Command \textrho unavailable in encoding T1" for pdflatex17/08 15:24
Saizanstelleg: the textgreek package might otherwise work17/08 15:31
stellegSaizan: thanks, that did work!17/08 15:32
stellegonly downside now is that in general the generated unicode characters don't seem to be monospaced :(17/08 15:32
stellegOh well, still much improved. Thanks for your help Saizan17/08 16:06
Saizanstelleg: cheers!17/08 19:21
lfishhello, I'm having a bit of a trouble with the induction principle over general inductive propositions, can you point me to some resource to understand it better?17/08 23:27

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