Def Lean.MVarId.introsWithBinderIdents

Modification history

2023-06-05 08:37

Mathlib/Tactic/Core.lean

feat: tactic `gcongr` for "relational congruence" (#3965) …

Added Lean.MVarId.introsWithBinderIdents View on Github →