Zulip Chat Archive
Stream: general
Topic: norm_cast coe_to_fun
Patrick Massot (Aug 22 2021 at 10:20):
@Rob Lewis I'm not sure: is norm_cast also intended to be used with has_coe_to_fun? A PR like #8661 has tons of lemmas that would be norm_cast lemmas.
Last updated: Dec 20 2023 at 11:08 UTC