metavariable

Stream: Is there code for X?

[Frédéric Le Roux]

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

[Rob Lewis]

In interactive mode or for metaprogramming?

[Rob Lewis]

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

[Frédéric Le Roux]

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

[Rob Lewis]

With what behavior? Failing if there is a metavariable?

[Frédéric Le Roux]

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)

[Rob Lewis]

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

[Frédéric Le Roux]

Great, many thanks!

[Rob Lewis]

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"