mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-09 11:44:56 +03:00
add runWriter helper
This commit is contained in:
parent
106f6b2d67
commit
29704102f0
@ -64,3 +64,6 @@ censor f m = pass $ do a <- m
|
||||
||| The Writer monad itself. See the MonadWriter interface
|
||||
Writer : Type -> Type -> Type
|
||||
Writer w a = WriterT w Identity a
|
||||
|
||||
runWriter : Writer w a -> (a, w)
|
||||
runWriter = runIdentity . runWriterT
|
||||
|
Loading…
Reference in New Issue
Block a user