git.iko.soy/Idris-dev
on master help sign in
Prelude: implement Functor for `Pair a`
ee7a3cbJacob Errington
libs/prelude/Prelude/Functor.idr+3
compare with master
unifiedsplit
@@ -1,5 +1,6 @@
1module Prelude.Functor
1module Prelude.Functor
2
2
3+import Builtins
3import Prelude.Basics
4import Prelude.Basics
4
5
5%access public export
6%access public export
@@ -22,3 +23,5 @@ infixl 4 <$>
22(<$>) : Functor f => (func : a -> b) -> f a -> f b
23(<$>) : Functor f => (func : a -> b) -> f a -> f b
23func <$> x = map func x
24func <$> x = map func x
24
25
26+Functor (Pair a) where
27+ map f (x, y) = (x, f y)
test/docs003/expected+1
@@ -10,6 +10,7 @@ Methods:
10
10
11 The function is Total
11 The function is Total
12Implementations:
12Implementations:
13+ Functor (Pair a)
13 Functor List
14 Functor List
14 Functor (IO' ffi)
15 Functor (IO' ffi)
15 Functor Stream
16 Functor Stream