git.iko.soy/Idris-dev
on master help sign in
Defined (<$) and ($>), analogous to Haskell's (<*) and (*>)
112f92astartling
lib/Prelude/Applicative.idr+9−1
compare with master
unifiedsplit
@@ -9,7 +9,15 @@ infixl 2 <$>
9
9
10class Functor f => Applicative (f : Type -> Type) where
10class Functor f => Applicative (f : Type -> Type) where
11 pure : a -> f a
11 pure : a -> f a
12− (<$>) : f (a -> b) -> f a -> f b
12+ (<$>) : f (a -> b) -> f a -> f b
13+
14+infixl 2 <$
15+(<$) : Applicative f => f a -> f b -> f a
16+a <$ b = fmap const a <$> b
17+
18+infixl 2 $>
19+($>) : Applicative f => f a -> f b -> f b
20+a $> b = fmap (const id) a <$> b
13
21
14class Applicative f => Alternative (f : Type -> Type) where
22class Applicative f => Alternative (f : Type -> Type) where
15 empty : f a
23 empty : f a