ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-20 21:49:53 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #4649 from zenntenn/makingtotal

Browse Source 
Makingtotal
This commit is contained in:
Niklas Larsson 2019-02-27 01:04:26 +01:00 committed by GitHub
commit 22f69e8abb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libs/base/Control/Catchable.idr
View File

@ -7,6 +7,7 @@ import Control.Monad.RWS
import Control.Monad.Trans
%access public export
%default total
interface Catchable (m : Type -> Type) t | m where
throw : t -> m a

2
libs/base/Data/IORef.idr
View File

@ -1,5 +1,7 @@
module Data.IORef
%default total
||| A mutable variable in the IO monad.
export
data IORef a = MkIORef a