/home/laney/.irssi/irclogs/Freenode/2011/#epigram/September.log

--- Log opened Thu Sep 01 00:00:54 2011
--- Day changed Sun Sep 04 2011
joe6copumpkin, you are on the this channel, too?04/09 04:30
copumpkinit would appear to be so :)04/09 04:30
augurwow04/09 04:40
augurcopumpkin04/09 04:40
augurguess he doesnt like you04/09 04:40
auguro_O04/09 04:40
--- Day changed Tue Sep 06 2011
guerrillaSo, I'm looking at "The view from the left" and one point confuses me. Are D-elim's elaborated to UTT or are they to be implemented in \iota-reduction in some other way?06/09 18:12
guerrillaif the latter, what would such a data structure for that look like? 06/09 18:13
--- Day changed Wed Sep 07 2011
pigworker_guerilla: Datatypes in UTT are generative. When you declare a datatype D, you get new canonical constants for D itself and D's constructors, and you get a new non-canonical constant D-elim, with its computation rules (\iota-reductions).07/09 09:55
--- Log closed Thu Sep 08 14:08:50 2011
--- Log opened Thu Sep 08 14:10:57 2011
-!- Irssi: #epigram: Total of 17 nicks [0 ops, 0 halfops, 0 voices, 17 normal]08/09 14:10
-!- Irssi: Join to #epigram was synced in 75 secs08/09 14:12
--- Log closed Thu Sep 08 16:11:08 2011
--- Log opened Thu Sep 08 16:11:15 2011
-!- Irssi: #epigram: Total of 19 nicks [0 ops, 0 halfops, 0 voices, 19 normal]08/09 16:11
-!- Irssi: Join to #epigram was synced in 99 secs08/09 16:12
--- Day changed Fri Sep 09 2011
guerrillapigworker: thanks09/09 00:02
--- Day changed Sat Sep 17 2011
tacticsWhat is the meaning of Forall P=>P in epigram?17/09 11:08
tacticsWould that be a shorthand for Forall (P:*)=>P?17/09 11:08
--- Log closed Sat Sep 24 04:09:46 2011

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