Stream: Coq users

Topic: Insert all implicit arguments maximally

spaceloop (Dec 18 2021 at 12:12):

Is it possible to ignore maximally/minimally inserted implicit argument declarations, and just insert all implicit arguments maximally?

spaceloop (Dec 18 2021 at 12:20):

I'd like to write things like concat ∘ (map f) instead of (@concat _) ∘ (map f), so I'd like to ignore that concat's implicit argument is defined as minimally inserted. Perhaps there are easier ways to deal with this?

Théo Zimmermann (Dec 19 2021 at 13:42):

I don't think there is a way to change the maximal status of implicit arguments for everything at once (and I'm not sure that it would be such a good idea) but you can override any implicit argument definition with the Arguments command: https://coq.inria.fr/refman/language/extensions/arguments-command.html

spaceloop (Dec 20 2021 at 10:16):

Thanks. I'd have to do that on a per-definition basis then, which is what I'm trying to avoid, e.g. all common helper functions from Coq.Lists.List. What problems do you foresee with changing the maximal status of all definitions (or perhaps on a per-module basis)?

Last updated: Oct 13 2024 at 01:02 UTC