Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: instance search in tactic


view this post on Zulip Johan Commelin (Oct 27 2020 at 13:13):

Is it possible to branch in a tactic depending on whether or not one can find a certain type class instance?

view this post on Zulip Johan Commelin (Oct 27 2020 at 13:14):

Suppose I have a G : Type in my context. I want to run tactic foo if [group G] and bar if [group_with_zero G].

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 13:19):

One way to do this is

(do to_expr ``(group %%G) >>= mk_instance, foo) <|> bar

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 13:19):

That is, mk_instance t succeeds if it can find an instance of the type class t.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 13:20):

try_core (mk_instance t) always succeeds, and returns an option expr (containing the synthesized instance).

view this post on Zulip Johan Commelin (Oct 27 2020 at 13:26):

Ok, thanks!

view this post on Zulip Mario Carneiro (Oct 27 2020 at 14:05):

you can also use mcond (succeeds (mk_instance t)) foo bar, which is similar to the try_core version (and has the advantage over the <|> version that errors in foo are not ignored)


Last updated: May 09 2021 at 23:10 UTC