search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

Typo in `Data.List.Relation.Unary.All` #2468

Closed jamesmckinna closed 2 months ago

jamesmckinna commented 2 months ago

Fixes #2467

No CHANGELOG.

Applies to master as well as to v2.1.1.

jamesmckinna commented 2 months ago

I just noticed that how/whenever this was merged previously, it seems to have been undone on master: (link copied just now) https://github.com/agda/agda-stdlib/blob/577008ed887eb9d33be6eb3b216ecfdd852667ff/src/Data/List/Relation/Unary/All.agda#L197 Not quite sure how/why this happens/happened!?

JacquesCarette commented 2 months ago

git blame says the current master for that line is from f0ef8a647a which is pre-fix. So it looks like it was indeed undone. Except that git log says that the latest merge into this file is indeed cc69ea07b !

JacquesCarette commented 2 months ago

Mystery solved: this problem occurs twice in this file, you fixed the one at line 118 previously but didn't catch the one at line 197 !!!