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

--- Day changed Wed Apr 19 2017
SuprDewdare there scenarios where using rewrite is necessary, or can it always circumvented by creating new functions and pattern matching?19/04 18:33
glguyrewrite is sugar for a with clause with two patterns19/04 18:33
SuprDewdah ok, thanks19/04 18:34
glguyhttp://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#rewrite19/04 18:34
ReinHWhat are {-+} {-(-} called and/or where can I read about them?19/04 18:54
ReinHAnd is there a way to manipulate them in agda-mode?19/04 19:21
ReinHI guess their use is idiomatic rather than some syntactic construction. Maybe this is just a pigworker thing?19/04 19:54
ReinHIn which case, I would like to see his emacs config.19/04 19:55
mietekReinH: lilnk?19/04 19:55
mieteklink*19/04 19:55
ReinHe.g., https://github.com/pigworker/CS410-16/blob/master/exercises/Ex1.agda#L203-L212 He uses them to comment out certain sections and he seems to have the markers integrated with emacs so he can twiddle them.19/04 19:56
ReinHI am like a little baby so I wasn't sure if this is an agda idiom or a pigworker idiolect19/04 19:56
ReinHmietek: ^19/04 19:56
mietekfunny. I haven’t seen these before.19/04 19:57
ReinHYeah, just pigworker things I guess19/04 19:57
mietek{-  ...  -}  is standard block comment notation19/04 19:57
ReinHYou can see him twiddle them in live coding videos19/04 19:57
mietekI would like a twiddle command, too19/04 19:57
ReinHYeah, I think it's a special use of comments that includes markers he defines so he can twiddle sections19/04 19:57
mietekgallais: ^^19/04 19:57
ReinHI thought maybe it was a universal agda idiom but apparently not19/04 19:58
ReinHit is rather clever, as is his wont19/04 19:58
gallaisIt's a pigworker thing. But I wish I knew the keystrokes to toggle them because it's really nice to give presentations19/04 20:12
ReinHmietek gallais: ask (pigworker) and ye shall receive https://github.com/pigworker/SSGEP-DataData/blob/master/comedy.el19/04 20:14
ReinH(I tweeted him)19/04 20:14
mietekneat19/04 20:16
ReinHmietek: yeah, and ofc it's simple enough even I could have written it19/04 20:16
mietekI know nothing of emacs19/04 20:16
ReinHI know almost nothing.19/04 20:17
gallaisnice19/04 20:17
gallaisthe only bit I know of emacs is because of Agda. No one wants to make the mode better so if you have feature envy, you have to implement them yourself.19/04 20:18
ReinHHmm, it's a bit wonky for me as written.19/04 20:18
ReinHI mean, so far agda-mode is pretty great compared to idris-mode, haskell-mode, etc. Only thing that compares with it really is proof general.19/04 20:20
ReinHOh, not wonky, just works differently than I expected. comment-in expects you to be above the region, comment-out expects you to be inside the region19/04 20:29
ReinHgallais: I modified it a bit https://gist.github.com/reinh/f7cbe38904b896516ebb808bbd542ae919/04 20:35

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