--- Day changed Thu Aug 24 2017
rntzis there a greatest-lower-bound operator for Level in agda?24/08 16:41
rntzthere's 24/08 16:41
rntzthere's \lub, which is least upper bound24/08 16:41
TanebThere isn't24/08 17:11
byorgeyrntz: curious what you would use it for24/08 18:21
rntzhm. I have a concrete use-case but it is hard to minimize.24/08 19:22
rntz(and I have found a workaround)24/08 19:22

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