Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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