Shea Levy (Oct 21 2020 at 12:43): Shea Levy (Oct 21 2020 at 12:43):Is there any way to say "by default, for any implicit argument of this type, use this tactic to try to fill it in"?
Paolo Giarrusso (Oct 21 2020 at 13:00):You could make that type a typeclass, and provide an Hint Extern for it.
Paolo Giarrusso (Oct 21 2020 at 13:01):But it's not a safe refactoring, and you also get any other instance: those declared as such, and any local assumptions.
Paolo Giarrusso (Oct 21 2020 at 13:02):(still probably what I'd try)
Paolo Giarrusso (Oct 21 2020 at 13:03):If you change the requirements quite a bit more, tactics-in-terms (ltac:(...)) might be relevant, if you haven't seen those
Shea Levy (Oct 21 2020 at 13:03):Yeah, this was my backup
Last updated: Oct 03 2023 at 02:34 UTC