| --- Day changed Sat Jun 17 2017 | ||
| colonelj | hi I am reading https://spin.atomicobject.com/2012/11/11/unifying-programming-and-math-the-dependent-type-revolution/ | 17/06 04:47 |
|---|---|---|
| colonelj | how do you actually define a type that represents the odd natural numbers in a language like Agda? | 17/06 04:47 |
| colonelj | I mean in a way that actually uses '2' and '%' operator | 17/06 04:50 |
| lambda-11235 | colonelj: You could do something like http://lpaste.net/356301. This is painful to use for proofs however. | 17/06 08:24 |
| lambda-11235 | An encoding like the one in https://brianmckenna.org/blog/plus_equals_even_take_2 is much nicer to use. | 17/06 08:25 |
| mietek | anyone familiar with the protocol Agda uses to communicate with emacs-mode? | 17/06 09:42 |
| mietek | I mean, with agda-mode for emacs | 17/06 09:43 |
| mietek | best thing I’ve found is https://github.com/banacorn/agda-mode/wiki/Conversations-between-Agda-&-agda-mode | 17/06 14:26 |
Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!