search

agda / agda-stdlib

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

Relation.Binary.PropositionalEquality over-use, #2345

Closed JacquesCarette closed 2 months ago

JacquesCarette commented 3 months ago

Many uses of Relation.Binary.PropositionalEquality (which is kind of 'fat' for such a low-level module) can usually be done instead as importing .Core …and/or .Properties instead.

jamesmckinna commented 2 months ago

Monumental effort! I couldn't find much to comment on where @MatthewDaggitt had not already done so, so I'm not entirely confident about giving an "Approve" review, without really getting the fine-toothed comb out, but in principle, I think: merge!

JacquesCarette commented 2 months ago

Thanks @jamesmckinna . I am hoping to deal with the comments from Matthew in the next couple of days.

While quite time consuming, this exercise was also quite soothing and entertaining. Helped discover many things I'd like to discuss for a 3.0 version. As well as having me look at many parts of the library that I had no clue existed.

jamesmckinna commented 2 months ago

@JacquesCarette you wrote:

While quite time consuming, this exercise was also quite soothing and entertaining. Helped discover many things I'd like to discuss for a 3.0 version. As well as having me look at many parts of the library that I had no clue existed.

Perhaps, as momentum builds around v2.1/v3.0 issues/PRs, we should open a shopping list issue for v3.0, consolidating the discussions currently scattered through the repo?