How does one write type f ~> g = forall i. f i -> g i in Idris?
@pigworker @ertesx @d_christiansen @acid2 In idris:
(~>) : {i : Type} -> (i -> Type) -> (i -> Type) -> Type
f ~> g = {i : _} -> f i -> g i
-
-
@edwinbrady I am apparently not allowed to use {i : _} there. Is Idris 0.9.15.1 too old? -
@acid2 Until someone hides my laptop or deletes my github account, Idris is probably always too old.
End of conversation
New conversation -
-
-
@edwinbrady Do you have implicit lambda now?@ertesx@d_christiansen@acid2 -
@pigworker@ertesx@d_christiansen@acid2 Yes. Not widely tested so I'd like to know if it works properly. - 2 more replies
New conversation -
-
-
@edwinbrady@pigworker@d_christiansen@acid2 Once feature of the RankNTypes version is that f ~> g takes another type argument. Same here? -
@edwinbrady@pigworker To elaborate: Let (f : {A} → B → C) does (f x) take another argument or is it of type C? - 4 more replies
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.