Commit 2024-07-01 20:25 4f76c653

View on Github →

feat: convert_to ty at h tactic (#14253) Extends convert_to to be able to operate on any location. When converting the type of a local hypothesis, new congruence goals come first. Suggested on Zulip.

Estimated changes

Modified Mathlib/Tactic/Convert.lean

modified def Lean.MVarId.convert

added def Lean.MVarId.convertLocalDecl

added def Mathlib.Tactic.elabTermForConvert

Modified test/convert.lean