diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b647d5114..fdbc040f2b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,8 @@ Bug-fixes re-exported in their full generality which would lead to unsolved meta variables at their use sites. +* In `Data.Maybe.Base` the fixity declaration of `_<∣>_` was missing. This has been fixed. + Non-backwards compatible changes -------------------------------- diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda index a26e3c102b..a9b4d819cb 100644 --- a/src/Data/Maybe/Base.agda +++ b/src/Data/Maybe/Base.agda @@ -100,6 +100,7 @@ just a >>= f = f a -- Alternative: <∣> +infixr 6 _<∣>_ _<∣>_ : Maybe A → Maybe A → Maybe A just x <∣> my = just x nothing <∣> my = my diff --git a/src/Function/Strict.agda b/src/Function/Strict.agda index e08796bb15..e0bcd697d5 100644 --- a/src/Function/Strict.agda +++ b/src/Function/Strict.agda @@ -20,7 +20,7 @@ private a b : Level A B : Set a -infixl 0 _!|>′_ _!|>′_ +infixl 0 _!|>_ _!|>′_ infixr -1 _$!_ _$!′_ ------------------------------------------------------------------------