Def Lean.MVarId.rintroWithPats

Modification history

2026-04-21 11:43
Mathlib/Tactic/Core.lean
feat(gcongr): support `rintro` patterns (#36314) …
Added Lean.MVarId.rintroWithPatsView on Github →