search

agda / agda-stdlib

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

Pull all 'show' routines into `X.Show` #2021

Open JacquesCarette opened 1 year ago

JacquesCarette commented 1 year ago

There are a number of places where Data.String (and friends) are used merely for show. This introduces spurious dependencies. I think all of these should be moved to sub-modules.

Taneb commented 1 year ago

Isn't this already the case? There's already-deprecated shows in Data.Rational and Data.Integer but I can't see any others outside of X.Show modules

JacquesCarette commented 1 year ago

See PR #2016 for a number of examples.