a338273 · Idris-dev · git.iko.soy

libs/base/Control/Catchable.idr−3

compare with master

unifiedsplit

@@ -1,8 +1,5 @@

1module Prelude.Catchable

2

3−import Prelude.List

4−import Prelude.Maybe

5−import Prelude.Either

6import Control.IOExcept

3import Control.IOExcept

7

4

8class Catchable (m : Type -> Type) t where

5class Catchable (m : Type -> Type) t where

libs/base/Control/IOExcept.idr−2

@@ -1,7 +1,5 @@

1module Control.IOExcept

2

3−import Prelude

4−

5-- An IO monad with exception handling

3-- An IO monad with exception handling

6

4

7data IOExcept : Type -> Type -> Type where

5data IOExcept : Type -> Type -> Type where

libs/base/Control/Monad/Identity.idr−4

@@ -1,9 +1,5 @@

1module Control.Monad.Identity

2

3−import Prelude.Functor

4−import Prelude.Applicative

5−import Prelude.Monad

6−

7public record Identity : Type -> Type where

3public record Identity : Type -> Type where

8 Id : (runIdentity : a) -> Identity a

4 Id : (runIdentity : a) -> Identity a

9

5

libs/base/Control/Monad/RWS.idr−3

@@ -1,12 +1,9 @@

1module Control.Monad.RWS

2

3−import Builtins

4import Control.Monad.Identity

3import Control.Monad.Identity

5import Control.Monad.State

4import Control.Monad.State

6import Control.Monad.Writer

5import Control.Monad.Writer

7import Control.Monad.Reader

6import Control.Monad.Reader

8−import Prelude.Monad

9−import Prelude.Functor

10

7

11%access public

8%access public

12

9

libs/base/Control/Monad/Reader.idr−3

@@ -2,9 +2,6 @@ module Control.Monad.Reader

2

3import Builtins

4import Control.Monad.Identity

5−import Prelude.Monad

6−import Prelude.Applicative

7−import Prelude.Functor

8

5

9%access public

6%access public

10

7

libs/base/Control/Monad/State.idr−2

@@ -1,8 +1,6 @@

1module Control.Monad.State

2

3import Control.Monad.Identity

4−import Prelude.Monad

5−import Prelude.Functor

6

4

7%access public

5%access public

8

6

libs/base/Control/Monad/Writer.idr−3

@@ -2,9 +2,6 @@ module Control.Monad.Writer

2

3import Builtins

4import Control.Monad.Identity

5−import Prelude.Monad

6−import Prelude.Applicative

7−import Prelude.Functor

8

5

9%access public

6%access public

10

7

libs/base/Data/Bits.idr−2

@@ -1,7 +1,5 @@

1module Data.Bits

2

3−import Prelude

4−

5%default total

3%default total

6

4

7divCeil : Nat -> Nat -> Nat

5divCeil : Nat -> Nat -> Nat

libs/base/Data/BoundedList.idr−2

@@ -1,7 +1,5 @@

1module Data.BoundedList

2

3−import Prelude

4−

5%access public

3%access public

6%default total

4%default total

7

5

libs/base/Data/Complex.idr+1−4

@@ -3,10 +3,7 @@

3-}

4

5

6−module Prelude.Complex

6+module Data.Complex

7−

8−import Builtins

9−import Prelude

10

7

11import Data.Floats

8import Data.Floats

12

9

libs/base/Data/Floats.idr−2

@@ -1,7 +1,5 @@

1module Data.Floats

2

3−import Prelude

4−

5%access public

3%access public

6%default total

4%default total

7

5

libs/base/Data/Morphisms.idr−2

@@ -1,7 +1,5 @@

1module Data.Morphisms

2

3−import Prelude

4−

5%access public

3%access public

6

4

7data Morphism : Type -> Type -> Type where

5data Morphism : Type -> Type -> Type where

libs/base/Data/SortedMap.idr−1

@@ -1,6 +1,5 @@

1module Data.SortedMap

2

3−import Prelude

4-- TODO: write merge and split

3-- TODO: write merge and split

5

4

6data Tree : Nat -> Type -> Type -> Type where

5data Tree : Nat -> Type -> Type -> Type where

libs/base/Data/SortedSet.idr−1

@@ -1,6 +1,5 @@

1module Data.SortedSet

2

3−import Prelude

4import Data.SortedMap

3import Data.SortedMap

5

4

6-- TODO: add intersection, union, difference

5-- TODO: add intersection, union, difference

libs/base/Data/Vect/Quantifiers.idr−2

@@ -1,7 +1,5 @@

1module Data.Vect.Quantifiers

2

3−import Prelude

4−

5data Any : (P : a -> Type) -> Vect n a -> Type where

3data Any : (P : a -> Type) -> Vect n a -> Type where

6 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)

4 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)

7 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)

5 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 @@

1module Debug.Trace

2

3−import Prelude

4−import IO

5−

6trace : String -> a -> a

3trace : String -> a -> a

7trace x val = unsafePerformIO (do putStrLn x; return val)

4trace x val = unsafePerformIO (do putStrLn x; return val)

8

5

libs/base/Language/Reflection.idr−2

@@ -1,7 +1,5 @@

1module Language.Reflection

2

3−import Prelude

4−

5%access public

3%access public

6

4

7data TTName = UN String

5data TTName = UN String

libs/base/Language/Reflection/Utils.idr−1

@@ -1,6 +1,5 @@

1module Language.Reflection.Utils

2

3−import Prelude

4import Language.Reflection

3import Language.Reflection

5

4

6--------------------------------------------------------

5--------------------------------------------------------

libs/base/Uninhabited.idr−2

@@ -1,7 +1,5 @@

1module Uninhabited

2

3−import Prelude

4−

5class Uninhabited t where

3class Uninhabited t where

6 total uninhabited : t -> _|_

4 total uninhabited : t -> _|_

7

5