search

agda / agda-stdlib

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

A number of `with` are not really needed #2363

Closed JacquesCarette closed 5 months ago

JacquesCarette commented 5 months ago

Many many were actually closer to needed, so left alone.

Some with were made clearer (to be merely pattern matches, but ones that caused various things to reduce, so with was the better idiom to use).

Basically the only ones that were not touched were the ones in Data.List.Base !!

JacquesCarette commented 5 months ago

Considered all, I'll enact about 2/3 of them.

jamesmckinna commented 5 months ago

Looks good! can we have a second review from someone please?

JacquesCarette commented 5 months ago

Thanks for the suggestions @gallais those did noticeably improve readability.