Jacques Carette

I do wonder if this is a genuine problem, at least in the context of Agda. [It might be!] It feels like a conundrum that is more philosophical: is stdlib...

> Returning to this comment, I wondered a lot about the first part: stdlib can often feel, in its structural organisation, that it is program-first (via Data.X.Base), and then prove...

Merging this now probably makes sense, but I'd want a concurring opinion - perhaps @gallais who has already looked at it?

I think there was an era of doing Agda development where some people were over-enthusiastic users of `with`, before its fragility was fully known/realized. I think there might have been...

I wonder if the recent features (not yet merged) to do more controlled abstraction and unfolding might be a more disciplined way to achieve this. That people may have done...

You'd definitely have to ask that on the agda board or the Zulip, the agda devs don't monitor stdlib chat all that closely.

Yes, absolutely. It so happens that it wasn't much needed up to now, but as we want to 'say more things', it very much becomes needed. So I'd welcome PRs...

All of these are typical warts of libraries that grow organically. Thanks for noticing and listing them explicitly. A bunch of small PRs fixing this would be most welcome. Definitely...

> Replace Data.List.Base as List and Data.List.Properties as List with shorter L aliases throughout the module for better readable proof While I happen to like that, this goes specifically against...

Another way to put it: if someone is arguing *for* `Maximum` and `Minimum` as being the "right" choices, backing that up with some references where those are the 'standard' names...