instance search in tactic

Stream: metaprogramming / tactics

[Johan Commelin]

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

[Johan Commelin]

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]

One way to do this is

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Johan Commelin]

Ok, thanks!

[Mario Carneiro]

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)