How does one write type f ~> g = forall i. f i -> g i in Idris?
-
-
Replying to @d_christiansen
@acid2 Note that you'll have to give it the i at most use sites.1 reply 0 retweets 0 likes -
Replying to @d_christiansen
@d_christiansen@acid2 The type seems incorrect and unnecessarily restricted, too: (~>) : (a -> Type) -> (a -> Type) -> a -> Type1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@d_christiansen@acid2 I thought (in agdris, apols) (~>) : (I -> Type) -> (I -> Type) -> Type (~>) {I} F G = (i : I) -> F i -> G i.2 replies 0 retweets 1 like -
Replying to @pigworker
@pigworker@d_christiansen@acid2 Wow, that looks weird. My Agda instinct does not like the pseudo-implicit i.1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@d_christiansen@acid2 In Agda, _~>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set F ~> G = forall {i} -> F i -> G i2 replies 0 retweets 0 likes -
Replying to @pigworker
@pigworker@ertesx@d_christiansen@acid2 In idris: (~>) : {i : Type} -> (i -> Type) -> (i -> Type) -> Type f ~> g = {i : _} -> f i -> g i3 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady I am apparently not allowed to use {i : _} there. Is Idris 0.9.15.1 too old?2 replies 0 retweets 0 likes
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.