Skip to content

Commit

Permalink
Update CHANGELOG.md
Browse files Browse the repository at this point in the history
Name change inherited from source update
  • Loading branch information
jamesmckinna authored Sep 30, 2024
1 parent 8391682 commit 22889c7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -314,7 +314,7 @@ Additions to existing modules

* In `Data.Product.Function.Dependent.Propositional`:
```agda
cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
```

* New lemma in `Data.Vec.Properties`:
Expand Down

0 comments on commit 22889c7

Please sign in to comment.