Commit 2020-04-18 00:48 6b095759
View on Github →feat(tactic/lint): lint for missing has_coe_to_fun instances (#2437) Enforces the library note "function coercion": https://github.com/leanprover-community/mathlib/blob/715be9f7466f30f1d4cbff4e870530af43767fba/src/logic/basic.lean#L69-L94 See #2434 for a recent PR where this issue popped up.