search

agda / agda-stdlib

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

fixes #2375 #2377

Closed jamesmckinna closed 1 month ago

jamesmckinna commented 2 months ago

NB contra @mechvel I have left f implicitly bound, on the prototype of Data.List.Relation.Binary.Sublist.Setoid.Properties.map⁺

Taneb commented 2 months ago

Is there a corresponding map- that could be added at the same time?

jamesmckinna commented 2 months ago

Is there a corresponding map- that could be added at the same time?

Not without injectivity off, I think... ... and might be considered mission creep/out of scope for this PR and its originating issue... (There's an implied time budget here... ;-))