--- Day changed Thu Sep 07 2017
AgdanoobI have installed agda in Ubuntu by sudo apt-get install agda and agda-mode . I have verified successful installation by running agda --interactions and agda -V07/09 05:23
AgdanoobBut i cannot get to work it in emacs07/09 05:24
AgdanoobWhen i use "agda-mode setup" command in terminal it says agda-mode command not found 07/09 05:25
AgdanoobPlease help me in this07/09 05:26
Agdanoobnevermind, got it worked. :)07/09 05:43
agguHello! Is anyone online atm?07/09 06:23
agguI just want to ask Is it possible for me to learn Agda is I am a beginner?07/09 06:26
agguPlease reply whenever someone gets time. I am waiting 07/09 06:29
subttleWould anyone be so kind as to inform me of the differences of using Fin vs. sized types?07/09 15:56
pgiarrussosubttle: sized types are often inferred and solved automatically. They also support infinite codata structures via infinite sizes, but still allow checking productivity (sizes are given by ordinal numbers)07/09 16:09
dolioDo you mean indexing by naturals?07/09 16:19
dolioI don't see how Fin is directly related to sized types.07/09 16:19
dolioAlso, I think the way to think about the difference is this...07/09 16:20
dolioWhen people index their types by a natural 'size', it's usually intended to give a specific size to each value.07/09 16:22
dolioBut that's not the point of sized types.07/09 16:22
dolioThe point of sized types is more like stratified formulae in New Foundations. You check that the equations you write have decreasing or increasing size in a certain way. Then you can throw away the particualr sizes involved for that definition.07/09 16:23
dolioBecause the stratification has guaranteed that the definition is sound locally.07/09 16:24
subttlepgiarrusso: I see, thank you07/09 17:10
subttledolio: hm, I did not mean to assert that they are related07/09 17:10
subttlebut thank you for the insight, I will think on that07/09 17:11

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