ModuleAgda-2.7.0.1Haskell2010
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₄ ```
- 1 value
- PackageAgda-2.7.0.1
- Exports1
- LanguageHaskell2010
- LicenceMIT
- SourceDoNotation.hs