Skip to content

Commit 618d838

Browse files
ncfavierandreasabel
authored andcommitted
Add _>>_ for IO.Primitive.Core (#2374)
This has to be in scope for desugaring `do` blocks that don't bind intermediate results.
1 parent 3d54042 commit 618d838

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed

CHANGELOG.md

+5
Original file line numberDiff line numberDiff line change
@@ -492,6 +492,11 @@ Additions to existing modules
492492
forever : IO ⊤ → IO ⊤
493493
```
494494

495+
* In `IO.Primitive.Core`:
496+
```agda
497+
_>>_ : IO A → IO B → IO B
498+
```
499+
495500
* In `Data.Word.Base`:
496501
```agda
497502
_≤_ : Rel Word64 zero

src/IO/Primitive/Core.agda

+3
Original file line numberDiff line numberDiff line change
@@ -36,3 +36,6 @@ postulate
3636
-- Haskell-style alternative syntax
3737
return : A IO A
3838
return = pure
39+
40+
_>>_ : IO A IO B IO B
41+
a >> b = a >>= λ _ b

0 commit comments

Comments
 (0)