Def Congr!.possiblyEqualTypes

Modification history

2023-07-28 11:36

Mathlib/Tactic/Congr!.lean

feat: make `congr!`'s typeEq plausibility heuristic consider binder info (#5900) …

Deleted Congr!.possiblyEqualTypes View on Github →

2023-03-16 17:38

Mathlib/Tactic/Congr!.lean

feat: improvements to `congr!` and `convert` (#2606) …

Added Congr!.possiblyEqualTypes View on Github →