Stream: Coq users

Topic: Tactic for filling in implicits?


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

view this post on Zulip Paolo Giarrusso (Oct 21 2020 at 13:00):

You could make that type a typeclass, and provide an Hint Extern for it.

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

view this post on Zulip Paolo Giarrusso (Oct 21 2020 at 13:02):

(still probably what I'd try)

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

view this post on Zulip Shea Levy (Oct 21 2020 at 13:03):

Yeah, this was my backup


Last updated: Jan 29 2023 at 05:03 UTC