Parametrized tactic unit

Stream: new members

[Martin Dvořák]

Is there any tutorial about defining a custom tactic unit that is parametrized by data?

I didn't find anything about it in https://leanprover-community.github.io/extras/tactic_writing.html but I suppose there must be a way to do it.

[Mario Carneiro]

what do you mean? Lots of tactics take and/or return arguments, like src#tactic.find_assumption