How does one write type f ~> g = forall i. f i -> g i in Idris?
@pigworker @ertesx @d_christiansen @acid2 Yes. Not widely tested so I'd like to know if it works properly.
-
-
@edwinbrady If {x : S} -> T is now a first class type, then there are weird unavoidable corners.@ertesx@d_christiansen@acid2 -
@pigworker@ertesx@d_christiansen@acid2 It's not quite first class. Far too fiddly… I must write down the rules I've implemented.
End of conversation
New conversation -
-
-
@edwinbrady Porting my stuff would be a good experiment. Might have time in the mythical summer.@ertesx@d_christiansen@acid2Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.