Stream: Coq users

Topic: Insert all implicit arguments maximally


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC