Add _>>_ for IO.Primitive.Core

This has to be in scope for desugaring `do` blocks that don't bind intermediate results.
agda · May 1, 2024 · f7c78e8 · f7c78e8
1 parent ea994a0
commit f7c78e8
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -492,6 +492,11 @@ Additions to existing modules
  forever : IO ⊤ → IO ⊤
  ```
 
+* In `IO.Primitive.Core`:
+ ```agda
+ _>>_ : IO A → IO B → IO B
+ ```
+
 * In `Data.Word.Base`:
  ```agda
  _≤_ : Rel Word64 zero

diff --git a/src/IO/Primitive/Core.agda b/src/IO/Primitive/Core.agda
@@ -36,3 +36,6 @@ postulate
 -- Haskell-style alternative syntax
 return : A → IO A
 return = pure
+
+_>>_ : IO A → IO B → IO B
+a >> b = a >>= λ _ → b