Agda.Syntax.DoNotation

Desugaring for do-notation. Uses whatever `_>>=_` and `_>>_` happen to be in scope.

Example:

``` 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₄ ```

Documentation

desugarDoNotation :: Range -> List1 DoStmt -> ScopeM Expr