Commit 2025-02-11 15:35 399891fd
View on Github →refactor: don't use lambdas in CoeFun
instances (#21405)
Hiding the lambdas behind a non-reducible toFun
or changing the CoeFun
instance to FunLike
prevents many lemmas (some simp) to have a lambda as their head symbol.
Arguably, those were misports because Lean 3's has_coe_to_fun
was not reducible. Whether or not those should have become FunLike
or CoeFun := ⟨semireducibleDef⟩
back then is unclear.
Zulip