set ≠ tactic.interactive.set

Stream: general

[Frédéric Le Roux]

I have the following problem. I would like to recognise the type set X by pattern matching in some tactic, like

private meta def analyse_expr_step  (e : expr) : tactic string :=
match e with
| `(set %%X)

But since I am in a tactic.interactive namespace, Lean thinks that setis the tactic tactic.interactive set. How can I refer to plain setin a tactic.interactive namespace ??

[Chris Hughes]

_root_.set

[Frédéric Le Roux]

Thanks!

[Alex J. Best]

What do people think of editing the error reporting for ambiguous overload in lean now to print the _root_ namespace? I've also forgotten this many times and don't see any reason not to do this.