Def Lean.Elab.Term.CoeImpl.mkFunCoe

Modification history

2022-11-19 03:04
Mathlib/Tactic/Coe.lean
fix: use new `coerce?` API (#652) …
Deleted Lean.Elab.Term.CoeImpl.mkFunCoeView on Github →
2022-08-24 13:39
Mathlib/Tactic/Coe.lean
feat: more coercion notations
Added Lean.Elab.Term.CoeImpl.mkFunCoeView on Github →