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

--- Day changed Mon Aug 14 2017
glguyI've been playing a bit with using ordinal arithmetic. [ω ∙ nat x + nat y] works out to be enough fuel for computing Ackermann(x,y) for example :) https://glguy.net/ord/Ord.Ackermann.html14/08 01:21
--- Log closed Mon Aug 14 02:06:58 2017
--- Log opened Mon Aug 14 02:07:07 2017
-!- Irssi: #agda: Total of 116 nicks [0 ops, 0 halfops, 0 voices, 116 normal]14/08 02:07
-!- Irssi: Join to #agda was synced in 112 secs14/08 02:08
glguyAnyone using spacemacs with Agda and know how to disable it's automatic indentation on paste? It has no idea how to indent Agda, so it just makes a mess of my code every time it triggers.14/08 06:25
glguyAh ha! found it. had to modify the agda layer to add14/08 06:38
glguy(defun agda/init-agda ()14/08 06:38
glguy  (add-to-list 'spacemacs-indent-sensitive-modes 'agda2-mode))14/08 06:38
rntzwhat's the difference between TERMINATING and NON_TERMINATING?14/08 18:48
rntzwhy can't I pattern match on coinductive types in agda?14/08 20:19
Eduard_Munteanurntz, it should work fine, how are you doing it?14/08 20:34
rntzEduard_Munteanu: I'm using agda 2.5.2, example: http://sprunge.us/ijWL14/08 20:38
rntzthe last line gives me an error, "Pattern matching on coinductive types is not allowed"14/08 20:38
Eduard_MunteanuHm, the coinductive record syntax is new to me.14/08 20:39
rntzah. yeah, by "coinductive types" I meant "coinductive records"14/08 20:40
Saizan_rntz: it breaks subject reduction in coq14/08 21:00
Saizan_http://strictlypositive.org/ObsCoin.pdf14/08 21:01

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