Custom intro

Stream: lean4

[Mac]

Is it possible to extend the intro tactic to more complex types? If so, how does one extend it?

[Chris B]

The rintro tactic in mathlib might give you some inspiration. https://leanprover-community.github.io/mathlib_docs/tactic/rcases.html#tactic.rintro

It looks like there's some built-in support for this kind of thing in Lean 4: https://leanprover.github.io/lean4/doc/tactics.html?highlight=intro#pattern-matching

[Mac]

I am looking to extend intro by perform actions on the object before binding, not pattern matching on the resulting binding. More specifically. for my type T, I want to make intro a expand to apply f; intro a