Def Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe

Modification history

2022-10-10 21:29
Mathlib/Tactic/Coe.lean
chore: long lines (#460)
Modified Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoeView on Github →
2022-08-24 13:39
Mathlib/Tactic/Coe.lean
feat: more coercion notations
Added Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoeView on Github →