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

--- Day changed Sat May 13 2017
SrPxWhy adding fix to the calculus of constructions makes it inconsistent? It seems like there is a consensus on that, but why? Where is the proof of that?13/05 05:20
SrPxOh never mind13/05 05:22
{AS} SrPx Actually you can add fix if you have Guarded Recursion in your type system13/05 05:58
{AS}SrPx: http://www.cse.chalmers.se/~vezzosi/vezzosi-lic.pdf13/05 05:59
{AS}SrPx: of course as you found out fix with the type (a->a)->a is inconsistent since fix id : \bot13/05 06:03
SrPxyep, reading it now thanks13/05 06:05
SrPxwait13/05 06:36
SrPxwas it been proven that it is impossible to have a O(1) predecessor for any encoding of ADTs on coc?13/05 06:36
{AS}SrPx: I am unsure, sorry13/05 08:05

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