--- Day changed Mon Feb 05 2018
arjen-jonathanDoes anyone know of any formal work related to the ".." shape irrelevance in Agda05/02 13:48
{AS}arjen-jonathan: http://www.cse.chalmers.se/~abela/icfp17-long.pdf05/02 14:04
arjen-jonathanThanks for the reference05/02 14:08
arjen-jonathanI did not know it treated irrelevance as well.05/02 14:09
{AS}arjen-jonathan: sure, I think this is the reason why they introduced it05/02 14:12
{AS}arjen-jonathan: otherwise, I think Saizan is a co-author05/02 14:12
{AS}so he might be more relevant to ask05/02 14:12
arjen-jonathanAh, in that case I should have known ;-)05/02 14:28

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