Def Lean.Elab.Term.CoeImpl.mkSortCoe

Modification history

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