moved Functor to its own Prelude submodule.
commit741145092c1583c015a4840a2d7f897d9013de47
authorstartling <tdixon51793@gmail.com>
dateFri 16 Nov 2012, 19:56 (14 years ago)
parent3d74fb2
lib/Prelude.idr+1
@@ -10,6 +10,7 @@ import Prelude.List
1010import Prelude.Maybe
1111import Prelude.Monad
1212import Prelude.Applicative
13+import Prelude.Functor
1314import Prelude.Either
1415import Prelude.Vect
1516import Prelude.Strings
lib/Prelude/Functor.idrnew file+4
@@ -0,0 +1,4 @@
1+module Prelude.Functor
2+
3+class Functor (f : Set -> Set) where
4+ fmap : (a -> b) -> f a -> f b
lib/Prelude/Monad.idr+1−3
@@ -4,6 +4,7 @@ module Prelude.Monad
44
55import Builtins
66import Prelude.List
7+import Prelude.Functor
78
89%access public
910
@@ -13,9 +14,6 @@ class Monad (m : Set -> Set) where
1314 return : a -> m a
1415 (>>=) : m a -> (a -> m b) -> m b
1516
16−class Functor (f : Set -> Set) where
17− fmap : (a -> b) -> f a -> f b
18−
1917class Monad m => MonadPlus (m : Set -> Set) where
2018 mplus : m a -> m a -> m a
2119 mzero : m a