0N/Avar a, b : Type

2362N/Atype M : Type -> Type

0N/A

0N/Aop __ >>= __ : M a * (a ->? M b) ->? M b

0N/A%binder(__ <- __ :. __)% %binder(do __ <- __ :. __)%

0N/A

0N/Avar p : M a; q : a -> M a

0N/A

0N/A. def do x <- p :. do y <- q x :. do z <- q y :. q z

0N/A