Skip to content

Commit c3d32b1

Browse files
committed
Update CHANGELOG for the new functions
1 parent 41aa705 commit c3d32b1

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

CHANGELOG.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,12 @@ Additions to existing modules
190190
^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
191191
```
192192

193+
* In `Data.Product.Properties`:
194+
```agda
195+
swap-↔ : (A × B) ↔ (B × A)
196+
_,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D)
197+
```
198+
193199
* In `Data.Vec.Properties`:
194200
```agda
195201
updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →

0 commit comments

Comments
 (0)