Specifying the motive(s) using the `induction` tactic

Stream: lean4

[Valentin Robert]

Hello all,

Is it possible to specify the motive(s) when using the induction tactic (in my case, using the provided eliminator), or do we only get this flexibility by manually applying the recursor?

[Kyle Miller]

It doesn't look like it. Here's the syntax for the induction tactic.

[Valentin Robert]

Thanks for the pointer!
Here's a permalink, since it's already moved in that file: https://github.com/leanprover/lean4/blob/34d8ecc0665136a370dea796bf36f5ebab983d21/src/Init/Notation.lean#L388-L390