fixes #2466: add equivalence proofs

agda / agda-stdlib

The Agda standard library

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

Other

585 stars 237 forks source link

fixes #2466: add equivalence proofs #2478

Closed jamesmckinna closed 2 months ago

jamesmckinna commented 2 months ago

NB.:

enabled by the refactoring in #2463 in terms of Data.List.Relation.Unary.All.Properties.Core
easy refactoring of the private lemma
Fairbairn threshold? The additions are (specialised) versions of imported lemmas.

JacquesCarette commented 2 months ago

On Fairbairn: my feeling is that the lemmas here are somehow "more findable" than the more general version, and so likely to be more useful. So I'm happy with this 'duplication'.