git.iko.soy/Idris-dev
on master help sign in
Add <$> as an alias for map
ff7214eDavid Raymond Christiansen
libs/prelude/Prelude/Functor.idr+8
compare with master
unifiedsplit
@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where
10 ||| @ m the morphism
10 ||| @ m the morphism
11 map : (m : a -> b) -> f a -> f b
11 map : (m : a -> b) -> f a -> f b
12
12
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+
13class Functor f => VerifiedFunctor (f : Type -> Type) where
21class Functor f => VerifiedFunctor (f : Type -> Type) where
14 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
22 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
15 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
23 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->