Is it possible to ignore maximally/minimally inserted implicit argument declarations, and just insert all implicit arguments maximally?
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?
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
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: Sep 23 2023 at 08:01 UTC