Alternative syntax in Dao.lean

Changes

1 changed files (+2/-1)

• Dao.lean
  • @@ -76,7 +76,8 @@ def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u}
    def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do - -- fs >>= (λ f ↦ as >>= λ a ↦ pure (f a)) + -- fs >>= λ f ↦ as >>= λ a ↦ pure (f a) + -- fs >>= λ f ↦ f <$> as return (← fs) (← as) class Monad' (m : Type → Type) where