@@ -16,12 +16,12 @@ interface Applicative m => Monad (m : Type -> Type) where
1616 ||| Also called `bind`.
1717 (>>=) : m a -> ((result : a) -> m b) -> m b
1818
19− ||| Also called `join` or mu
20− flatten : m (m a) -> m a
19+ ||| Also called `flatten` or mu
20+ join : m (m a) -> m a
2121
2222 -- default implementations
23− (>>=) x f = flatten (f <$> x)
24− flatten x = x >>= (\y => y)
23+ (>>=) x f = join (f <$> x)
24+ join x = x >>= (\y => y)
2525
2626||| For compatibility with Haskell. Note that monads are **not** free to
2727||| define `return` and `pure` differently!