Commit 2022-10-24 02:14 467222f9

View on Github →

feat: port convert tactic (#492)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Convert.lean

added def Lean.MVarId.congrN'

added def Lean.MVarId.convert

Created test/convert.lean