7411450 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

moved Functor to its own Prelude submodule.

7411450startling14 years ago

lib/Prelude.idr+1

@@ -10,6 +10,7 @@ import Prelude.List

10import Prelude.Maybe

11import Prelude.Monad

12import Prelude.Applicative

13+import Prelude.Functor

13import Prelude.Either

14import Prelude.Either

14import Prelude.Vect

15import Prelude.Vect

15import Prelude.Strings

16import Prelude.Strings

lib/Prelude/Functor.idrnew file+4

@@ -0,0 +1,4 @@

1+module Prelude.Functor

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

5import Builtins

6import Prelude.List

7+import Prelude.Functor

8%access public

9%access public

@@ -13,9 +14,6 @@ class Monad (m : Set -> Set) where

13 return : a -> m a

14 return : a -> m a

14 (>>=) : m a -> (a -> m b) -> m b

15 (>>=) : m a -> (a -> m b) -> m b

16−class Functor (f : Set -> Set) where

17− fmap : (a -> b) -> f a -> f b

18−

19class Monad m => MonadPlus (m : Set -> Set) where

17class Monad m => MonadPlus (m : Set -> Set) where

20 mplus : m a -> m a -> m a

18 mplus : m a -> m a -> m a

21 mzero : m a

19 mzero : m a