Zulip Chat Archive

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

Johan Commelin (Oct 27 2020 at 13:26):

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: Dec 20 2023 at 11:08 UTC