somethig like a typo in lib-2.1.1-rc2

agda / agda-stdlib

The Agda standard library

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

Other

570 stars 233 forks source link

somethig like a typo in lib-2.1.1-rc2 #2467

Closed mechvel closed 1 week ago

mechvel commented 2 weeks ago

Data/List/Relation/Unary/All.agda starts with

All.agda:module _(S : Setoid a ℓ) ...

Probably it is better to set a space after _

jamesmckinna commented 2 weeks ago

Just a note for @MatthewDaggitt : #2468 has now been merged in to master (thanks @Taneb !) but should also be merged into your Agda-v2.7.0-compatible v2.1.1 branch?

MatthewDaggitt commented 1 week ago

I don't think a minor typo really needs to be merged in v2.1.1 unless there's some important bug that I'm missing?

jamesmckinna commented 1 week ago

Fine by me! No 'bug' as such at all...

mechvel commented 1 week ago

I do not know, may be to join to other changes and to merge to future versions.

jamesmckinna commented 1 week ago

@mechvel v2.1.1 is a compatibility release towards a mandatory upgrade from v2.2 onwards to Agda-v2.7.0, so I agree with @MatthewDaggitt that it's fine that the typo has been corrected (only) for v2.2...