Remove needless Prelude imports
commita3382730f5422b372d6324860675b0246a7ffcd3
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 22 Nov 2013, 16:15 (13 years ago)
parent90eb6a2
libs/base/Control/Catchable.idr−3
@@ -1,8 +1,5 @@
11module Prelude.Catchable
22
3−import Prelude.List
4−import Prelude.Maybe
5−import Prelude.Either
63import Control.IOExcept
74
85class Catchable (m : Type -> Type) t where
libs/base/Control/IOExcept.idr−2
@@ -1,7 +1,5 @@
11module Control.IOExcept
22
3−import Prelude
4−
53-- An IO monad with exception handling
64
75data IOExcept : Type -> Type -> Type where
libs/base/Control/Monad/Identity.idr−4
@@ -1,9 +1,5 @@
11module Control.Monad.Identity
22
3−import Prelude.Functor
4−import Prelude.Applicative
5−import Prelude.Monad
6−
73public record Identity : Type -> Type where
84 Id : (runIdentity : a) -> Identity a
95
libs/base/Control/Monad/RWS.idr−3
@@ -1,12 +1,9 @@
11module Control.Monad.RWS
22
3−import Builtins
43import Control.Monad.Identity
54import Control.Monad.State
65import Control.Monad.Writer
76import Control.Monad.Reader
8−import Prelude.Monad
9−import Prelude.Functor
107
118%access public
129
libs/base/Control/Monad/Reader.idr−3
@@ -2,9 +2,6 @@ module Control.Monad.Reader
22
33import Builtins
44import Control.Monad.Identity
5−import Prelude.Monad
6−import Prelude.Applicative
7−import Prelude.Functor
85
96%access public
107
libs/base/Control/Monad/State.idr−2
@@ -1,8 +1,6 @@
11module Control.Monad.State
22
33import Control.Monad.Identity
4−import Prelude.Monad
5−import Prelude.Functor
64
75%access public
86
libs/base/Control/Monad/Writer.idr−3
@@ -2,9 +2,6 @@ module Control.Monad.Writer
22
33import Builtins
44import Control.Monad.Identity
5−import Prelude.Monad
6−import Prelude.Applicative
7−import Prelude.Functor
85
96%access public
107
libs/base/Data/Bits.idr−2
@@ -1,7 +1,5 @@
11module Data.Bits
22
3−import Prelude
4−
53%default total
64
75divCeil : Nat -> Nat -> Nat
libs/base/Data/BoundedList.idr−2
@@ -1,7 +1,5 @@
11module Data.BoundedList
22
3−import Prelude
4−
53%access public
64%default total
75
libs/base/Data/Complex.idr+1−4
@@ -3,10 +3,7 @@
33-}
44
55
6−module Prelude.Complex
7−
8−import Builtins
9−import Prelude
6+module Data.Complex
107
118import Data.Floats
129
libs/base/Data/Floats.idr−2
@@ -1,7 +1,5 @@
11module Data.Floats
22
3−import Prelude
4−
53%access public
64%default total
75
libs/base/Data/Morphisms.idr−2
@@ -1,7 +1,5 @@
11module Data.Morphisms
22
3−import Prelude
4−
53%access public
64
75data Morphism : Type -> Type -> Type where
libs/base/Data/SortedMap.idr−1
@@ -1,6 +1,5 @@
11module Data.SortedMap
22
3−import Prelude
43-- TODO: write merge and split
54
65data Tree : Nat -> Type -> Type -> Type where
libs/base/Data/SortedSet.idr−1
@@ -1,6 +1,5 @@
11module Data.SortedSet
22
3−import Prelude
43import Data.SortedMap
54
65-- TODO: add intersection, union, difference
libs/base/Data/Vect/Quantifiers.idr−2
@@ -1,7 +1,5 @@
11module Data.Vect.Quantifiers
22
3−import Prelude
4−
53data Any : (P : a -> Type) -> Vect n a -> Type where
64 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
75 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
libs/base/Debug/Trace.idr−3
@@ -1,8 +1,5 @@
11module Debug.Trace
22
3−import Prelude
4−import IO
5−
63trace : String -> a -> a
74trace x val = unsafePerformIO (do putStrLn x; return val)
85
libs/base/Language/Reflection.idr−2
@@ -1,7 +1,5 @@
11module Language.Reflection
22
3−import Prelude
4−
53%access public
64
75data TTName = UN String
libs/base/Language/Reflection/Utils.idr−1
@@ -1,6 +1,5 @@
11module Language.Reflection.Utils
22
3−import Prelude
43import Language.Reflection
54
65--------------------------------------------------------
libs/base/Uninhabited.idr−2
@@ -1,7 +1,5 @@
11module Uninhabited
22
3−import Prelude
4−
53class Uninhabited t where
64 total uninhabited : t -> _|_
75