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

--- Day changed Sat Jun 17 2017
coloneljhi I am reading https://spin.atomicobject.com/2012/11/11/unifying-programming-and-math-the-dependent-type-revolution/17/06 04:47
coloneljhow do you actually define a type that represents the odd natural numbers in a language like Agda?17/06 04:47
coloneljI mean in a way that actually uses '2' and '%' operator17/06 04:50
lambda-11235colonelj: You could do something like http://lpaste.net/356301. This is painful to use for proofs however.17/06 08:24
lambda-11235An encoding like the one in https://brianmckenna.org/blog/plus_equals_even_take_2 is much nicer to use.17/06 08:25
mietekanyone familiar with the protocol Agda uses to communicate with emacs-mode?17/06 09:42
mietekI mean, with agda-mode for emacs17/06 09:43
mietekbest thing I’ve found is https://github.com/banacorn/agda-mode/wiki/Conversations-between-Agda-&-agda-mode17/06 14:26

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