Modernising `Data.Nat.Properties`

agda / agda-stdlib

The Agda standard library

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

Other

583 stars 236 forks source link

Modernising `Data.Nat.Properties` #2088

Closed jamesmckinna closed 11 months ago

jamesmckinna commented 1 year ago

Two quick thoughts, plus a placeholder:

[ ] currently, there is no use of variables !
[ ] suc-injective can be made lazier by redefining it as cong pred, and systematically replacing uses of that compound elsewhere?
[ ] anything else?

NB this is intended to be cosmetic for v2.0, not the systematic overhaul envisaged by @JacquesCarette in #1925

Note to self: could be folded into any PR addressing #2087

jamesmckinna commented 11 months ago

I'm sure that this sort of issue will recur, but closing this now (and should have, after #2089).

MatthewDaggitt commented 11 months ago

@jamesmckinna when you close issues because a PR has addressed them, can you check that there's the correct Milestone added and the PR is linked against in the Development box (both on the RHS). Makes it a little easier to sort and filter historical issues when doing archaeology!

jamesmckinna commented 11 months ago

Certainly! Sorry to have missed your comment until now.