antiquotations in `[ ... ] tactics?

Stream: general

[Scott Morrison]

I've never been clear on whether it's possible to put antiquotation in `[ ... ] tactics.

[Scott Morrison]

Does anyone know?

[Scott Morrison]

Sometimes in a tactic I'd love to just be able to call the interactive version of induction, writing something like
`[induction %%e using trunc.rec_on_subsingleton].

[Scott Morrison]

rather than having to read the call syntax of the non-interactive induction tactic.