DoLikeNotation.agda

open import Category.Monad

module DoLikeNotation {l M} (monad : RawMonad {l} M) where

open RawMonad monad

bind-syntax = _>>=_

syntax bind-syntax F (λ x → G) = ∣ x ← F ∣ G

test : {A B C : Set l} → M A → (A → M B) → (A → B → M C) → M C
test F G H = ∣ x ← F
           ∣ ∣ y ← G x
           ∣ ∣ y ← G x
           ∣ ∣ _ ← F
             ∣ H x y