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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.DoNotation

Description

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 Source #