search

agda / agda-stdlib

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

move `_≗_` from `Relation.Binary.PropositionalEquality` to `*.Core` #2331

Closed JacquesCarette closed 3 months ago

JacquesCarette commented 3 months ago

It has a very straightforward definition (if you unwind the current overly complex one) and is used a fair amount, which then drags in quite a bit more than is needed. In particular, Data.Product.Properties is otherwise very simple, but lies higher up in the dependency graph due to this single definition.

MatthewDaggitt commented 3 months ago

This is fine to do!

MatthewDaggitt commented 3 months ago

And yes that definition is definitely a little overly complex!

jamesmckinna commented 3 months ago

I agree with each of you!