--- Day changed Thu Feb 01 2018
carteram I doing something fundamentally impredicative in this code or am I overlooking something obvious? https://gist.github.com/cartazio/373eaa1ab726b2f6e651777a44b3f2b101/02 22:12
mietekcarter: `Pair Set Set !=< Set₁`01/02 23:02
mietekyou’re giving an inhabitant of a type where you wanted to give a type01/02 23:03
carterOhhhh. 01/02 23:03
pgiarrussoalso, I don't think Pair needs the Level.suc, or do I miss something?01/02 23:04
mietekindeed01/02 23:04
carterthanks!01/02 23:05
pgiarrussobut yeah, SignedPair should take Pair a b, not mkPair a b01/02 23:05
carterthat fixes everything01/02 23:05
carterpgiarrusso:  mietek  thank you so much!01/02 23:05
carterpgiarrusso:  mietek  thank you so much!01/02 23:06
mietekall right01/02 23:06

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