git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4649 from zenntenn/makingtotal
22f69e8Niklas Larsson
libs/base/Control/Catchable.idr+1
compare with master
unifiedsplit
@@ -7,6 +7,7 @@ import Control.Monad.RWS
7import Control.Monad.Trans
7import Control.Monad.Trans
8
8
9%access public export
9%access public export
10+%default total
10
11
11interface Catchable (m : Type -> Type) t | m where
12interface Catchable (m : Type -> Type) t | m where
12 throw : t -> m a
13 throw : t -> m a
libs/base/Data/IORef.idr+2
@@ -1,5 +1,7 @@
1module Data.IORef
1module Data.IORef
2
2
3+%default total
4+
3||| A mutable variable in the IO monad.
5||| A mutable variable in the IO monad.
4export
6export
5data IORef a = MkIORef a
7data IORef a = MkIORef a