add_theorem_by

Stream: general

[Jakob von Raumer]

Why does this fail?

meta  def  foo : tactic unit :=
do tactic.add_theorem_by `bar [] (expr.const `unit []) (do tactic.constructor, return ()),
tactic.add_theorem_by `baz [] (expr.const `unit []) (do
bar ← tactic.get_local `bar,
tactic.exact bar,
return ()),
return ()

[Simon Hudon]

What error do you get?

[Jakob von Raumer]

"get_local tactic failed, unknown 'bar'"

[Simon Hudon]

Ah I see! You need resolve_name

[Simon Hudon]

get_local is only for local constants

[Jakob von Raumer]

Is there a resource for more beautiful fresh local names than mk_fresh_name?

[Mario Carneiro]

yes, I think it is called get_unused_name