## Stream: metaprogramming / tactics

### Topic: instance search in tactic

#### 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?

#### 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].

#### Gabriel Ebner (Oct 27 2020 at 13:19):

One way to do this is

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


#### 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.

#### Gabriel Ebner (Oct 27 2020 at 13:20):

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

Ok, thanks!

#### 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