--- Day changed Tue Mar 07 2017
mietekrntz: can you have functions in Agda which are not strictly positive?07/03 09:21
Saizanrntz: one way is to quantify over containers, another is to use an inductive description of the functions you want07/03 10:34
Saizanmietek: "\ (X : Set) -> X -> X" is not even positive!07/03 10:35
mietekSaizan: ah, it’s only when we try to define a new datatype that would stand for X that Agda complains, right?07/03 10:36
Saizanmietek: yeah, data D : Set where con : (D -> D) -> D would be caught07/03 10:36
rntzSaizan: quantify over containers? what is a container?07/03 11:48
rntzah, Data.Container?07/03 11:51
Saizanrntz: yep07/03 12:47
gallaisfor the "inductive description of the functions", see https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf07/03 13:37
quchenHello everyone! I’m having trouble using (subst : x=y -> P x -> P y). My main problem doing proofs is that I can’t seem to scope into expressions very well, and I suspect subst does that.07/03 18:35
quchenConsider for example the theorem »foo : ∀ m n -> succ (m + n) = succ (n + m)«.07/03 18:36
quchenThis is easy enough to prove directly, but I’m wondering how I can do it in terms of subst.07/03 18:36
quchenAm I on the right track here?07/03 18:36
quchenIf I apply commutativity of addition as the first argument to subst, which makes sense to me since the result depends on it, I get07/03 18:37
quchenfoo m n = subst (comm-+ m n) ?07/03 18:37
quchenAnd here I’m stuck.07/03 18:37
quchenI basically don’t know how to generate and access the »P« from the »subst« definition.07/03 18:38
quchenI feel like my »?« should be something like 07/03 18:40
quchen(λ x -> succ x ≡ succ x) (m + n)07/03 18:40
quchenThis would make »P = (λ x -> succ x ≡ succ x)«07/03 18:41
vorgangI need help installing the emacs mode. There's no "agda-mode" command...07/03 19:47
vorgangoh wait, actually there is07/03 19:48
serendependyvorgang: How far along are you with the instructions here: https://github.com/agda/agda#installing-agda07/03 19:48
vorgangserendependy: agda itself should be installed (via cabal I believe)07/03 19:50
vorgangsomehow ~/.cabal/bin is now in $PATH, not sure why07/03 19:51
serendependyHave you run agda-mode setup from the command line?07/03 19:52
vorgangyup, that finally worked a minute ago07/03 19:52
vorgangwhere does the .emacs file go? I use ~/.emacs.d/init.el, is that equivalent?07/03 19:53
serendependyvorgang: I believe agda-mode will write to ~/.emacs07/03 19:53
vorgangok I have an emacs window that says (Agda), guess it's working07/03 19:55
vorgangalthough there's no syntax highlighting07/03 20:00
serendependyvorgang: C-c C-l to load an Agda file (including highlighting)07/03 20:03
vorgangok got syntax highlighting now after C-c C-x C-l07/03 20:03
vorgangyup07/03 20:03
vorgangquite nice! thanks!07/03 20:03
serendependyvorgang: More about the Emacs mode (and the docs in general): http://agda.readthedocs.io/en/latest/tools/emacs-mode.html07/03 20:04
serendependynp07/03 20:04
mietekemacs is the only program I use that regularly crashes while it is in the background doing nothing07/03 21:40
mietek*sigh*07/03 21:40

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