git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4335 from aiya000/feature/move-ignore-func-to-prelude-functor
6d7fd7bAhmad Salim Al-Sibahi
libs/prelude/Prelude/Functor.idr+4
compare with master
unifiedsplit
@@ -23,5 +23,9 @@ infixr 4 <$>
23(<$>) : Functor f => (func : a -> b) -> f a -> f b
23(<$>) : Functor f => (func : a -> b) -> f a -> f b
24func <$> x = map func x
24func <$> x = map func x
25
25
26+||| Run something for effects, throwing away the return value
27+ignore : Functor f => f a -> f ()
28+ignore x = map (const ()) x
29+
26Functor (Pair a) where
30Functor (Pair a) where
27 map f (x, y) = (x, f y)
31 map f (x, y) = (x, f y)
libs/pruviloj/Pruviloj/Core.idr−4
@@ -7,10 +7,6 @@ import Language.Reflection.Utils
7
7
8%access public export
8%access public export
9
9
10−||| Run something for effects, throwing away the return value
11−ignore : Functor f => f a -> f ()
12−ignore x = map (const ()) x
13−
14||| Do nothing
10||| Do nothing
15skip : Applicative f => f ()
11skip : Applicative f => f ()
16skip = pure ()
12skip = pure ()