Add <$> as an alias for map
commitff7214eff142ee13461b3c21ece9ef5d5f6b7813
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 2 Mar 2015, 10:57 (12 years ago)
parent48d6a6b
libs/prelude/Prelude/Functor.idr+8
@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where
1010 ||| @ m the morphism
1111 map : (m : a -> b) -> f a -> f b
1212
13+infixl 4 <$>
14+
15+||| An infix alias for `map`: the action of a functor on morphisms.
16+||| @ f the functor
17+||| @ m the morphism
18+(<$>) : Functor f => (m : a -> b) -> f a -> f b
19+m <$> x = map m x
20+
1321class Functor f => VerifiedFunctor (f : Type -> Type) where
1422 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
1523 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->