@edwinbrady Does the #idris version in https://gist.github.com/phadej/8525849 work because of universe polymorphism for all definitions, compared to #coq?
@phadej It probably shouldn't work. Universe checking isn't very well exercised.
-
-
@edwinbrady However the "written out" example in Coq works? And also application, I guess I have to go thru the example with pen and paper. -
@phadej Probably the best thing to do is note it on the issue tracker so that someone can have a proper look at it. Pretty sure it's a bug.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.