Commit 2022-08-24 13:39 9d27bb95

View on Github →

feat: more coercion notations

Estimated changes

Modified Mathlib/Tactic/Coe.lean

added def Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe

added def Lean.Elab.Term.CoeImpl.mkFunCoe

added def Lean.Elab.Term.CoeImpl.mkSortCoe