mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
clarify toMaybeT
docstring
This commit is contained in:
parent
c0ac024114
commit
40d4cd898b
@ -68,7 +68,9 @@ public export
|
||||
fromMaybeT : Monad m => m a -> MaybeT m a -> m a
|
||||
fromMaybeT v x = runMaybeT x >>= maybe v pure
|
||||
|
||||
||| Return a value if a condition is met, or else no value.
|
||||
||| Return a value if a condition is met, or else no value. The condition
|
||||
||| only affects whether the `Maybe` produces a value; the effect is run
|
||||
||| either way.
|
||||
|||
|
||||
||| This is a version of `toMaybe` lifted to work with `MaybeT`.
|
||||
public export
|
||||
|
Loading…
Reference in New Issue
Block a user