Agda-2.6.0: A dependently typed functional programming language and proof assistant

Desugaring for do-notation. Uses whatever _>>=_ and _>>_ happen to be in scope.
 foo = do x ← m₁ m₂ just y ← m₃ where nothing → m₄ let z = t m₅  desugars to  foo = m₁ >>= λ x → m₂ >> m₃ >>= λ where just y → let z = t in m₅ nothing → m₄