Zulip Chat Archive

Stream: Is there code for X?

Topic: metavariable


view this post on Zulip Frédéric Le Roux (Dec 16 2020 at 22:22):

Is there a tactic that check if the target contains a metavariable?

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:26):

In interactive mode or for metaprogramming?

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:26):

expr.has_meta_var <$> tactic.target for the latter.

view this post on Zulip Frédéric Le Roux (Dec 16 2020 at 22:26):

It would be better for me in interactive mode...

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:27):

With what behavior? Failing if there is a metavariable?

view this post on Zulip Frédéric Le Roux (Dec 16 2020 at 22:27):

Yes, that would be perfect
(I want to combine this with any tactic, to avoid using a tactic if it leads to metavariables in the target)

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:30):

I don't think it's in the library but

meta def tactic.interactive.no_meta_vars : tactic unit :=
mwhen (expr.has_meta_var <$> tactic.target) $ tactic.fail "target contains metavars"

example :  x : , x = 0 :=
begin
  existsi _,
  no_meta_vars
end

view this post on Zulip Frédéric Le Roux (Dec 16 2020 at 22:31):

Great, many thanks!

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:34):

Better:

meta def tactic.interactive.no_meta_vars : tactic unit :=
mwhen (expr.has_meta_var <$> (tactic.target >>= tactic.instantiate_mvars)) $ tactic.fail "target contains metavars"

Last updated: May 17 2021 at 16:26 UTC