Zulip Chat Archive
Stream: mathlib4
Topic: unfold_coes
Patrick Massot (Aug 31 2023 at 22:20):
What is the status of porting docs3#tactic.interactive.unfold_coes? I'm porting the sphere eversion project and find a lot of those.
Patrick Massot (Aug 31 2023 at 22:22):
But to be honest I can often simply remove that line, so maybe the new coercion system makes it useless.
Yury G. Kudryashov (Sep 01 2023 at 03:12):
Most coes are now unfolded at parsing time.
Yury G. Kudryashov (Sep 01 2023 at 03:13):
Two exceptions I can think of are FunLike.coe and SetLike.coe.
Last updated: Dec 20 2023 at 11:08 UTC