added changelog information

agda · Feb 18, 2024 · d72b95d · d72b95d
1 parent d855283
commit d72b95d
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -187,3 +187,8 @@ Additions to existing modules
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
+
+* Added new definition in `Data.Maybe.Relation.Unary.AllBoth`:
+  ```agda
+  data AllBoth (P : Pred A p) (Q : Set q) : Pred (Maybe A) (a ⊔ p ⊔ q)
+  ```