Def Mathlib.Tactic.TermCongr.mkHCongrWithArity'

Modification history

2023-09-10 13:09

Mathlib/Tactic/TermCongr.lean

refactor: re-home some meta code (#6921)

Deleted Mathlib.Tactic.TermCongr.mkHCongrWithArity'View on Github →

2023-08-27 12:05

Mathlib/Tactic/TermCongr.lean

feat: `congr(...)` congruence quotations and port `congrm` tactic (#2544) …

Added Mathlib.Tactic.TermCongr.mkHCongrWithArity'View on Github →