calling a tactic "by name"?

Stream: general

[Scott Morrison]

I'd like to tell one of my tactics to try calling norm_num, but not have to import norm_num myself.

[Scott Morrison]

In particular, I'd like my call to norm_num to just fail if norm_num hasn't actually been imported by the time I invoke it.

[Scott Morrison]

Is there some trickery with pre-expressions that will let me do this?

[Keeley Hoek]

Definitely.

[Keeley Hoek]

You want to eval_expr an expr which corresponds to the norm_num tactic, which you build only if you can resolve the name in tactic.interactive.

[Keeley Hoek]

Then you can just execute it.

[Scott Morrison]

Oh.. tidy.lean actually contains name_to_tactic

[Scott Morrison]

which maybe does exactly this

[Mario Carneiro]

You can more reliably test existence using resolve_name

[Scott Morrison]

I should git blame that line and see if I wrote it ...

[Mario Carneiro]

If you just eval_expr it then you won't be able to tell whether it failed because norm_num failed or norm_num doesn't exist

[Scott Morrison]

In this use case, I actually don't care much. :-)

[Keeley Hoek]

Yeah sorry to be clear, I meant to check for existence before you build the expr. But ok.

[Keeley Hoek]

By the way, that function name_to_tactic looks broken to me. I'm going to push a fix. (If I recall =ₐ means equals-ignoring-binders, which is just wrong.) Nope, it's equals ignoring binder names! This does nothing in this case, but I suppose makes more sense.