These are both called by Core.Core in Blodwen,
which I also want to make %default total
commitd27b255dd2e29cfa3f9b6123ad0b623940822535
authorzenntenn <zenten@zenten.ca>
dateSat 26 Jan 2019, 11:25 (8 years ago)
parenta33905e
libs/base/Control/Catchable.idr+1
@@ -7,6 +7,7 @@ import Control.Monad.RWS
77import Control.Monad.Trans
88
99%access public export
10+%default total
1011
1112interface Catchable (m : Type -> Type) t | m where
1213 throw : t -> m a
libs/base/Data/IORef.idr+2
@@ -1,5 +1,7 @@
11module Data.IORef
22
3+%default total
4+
35||| A mutable variable in the IO monad.
46export
57data IORef a = MkIORef a