Skip to content

Commit

Permalink
Fix typo in CHANGELOG (#5905)
Browse files Browse the repository at this point in the history
  • Loading branch information
person-with-a-username committed May 14, 2022
1 parent 2c0cfae commit 257a324
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 @@ -30,7 +30,7 @@ Language
([#4786](https://github.com/agda/agda/issues/4786)).

For instance, the type of the constructor `c` below is now `{@0 A :
Set} → D A`, and the type of the record field `R.f` is {@0 A : Set}
Set} → D A`, and the type of the record field `R.f` is `{@0 A : Set}
→ R A → A`:
```agda
data D (A : Set) : Set where
Expand Down

0 comments on commit 257a324

Please sign in to comment.