feat: display coercions with a type ascription

[tonyxty]

This PR adds a new delab option pp.coercions.types which, when enabled, will display all coercions with an explicit type ascription.

Link to Zulip discussion

Towards #4315

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 14:37:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 5a99cb326c9e9052e135cc63ed02b63371cff6d3. (2024-11-19 01:49:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-20 01:03:11)

[kmill]

By the way, I edited the PR description to say "towards" instead of "closes" because I think there are things we can do to pp.analyze once we have the pp config flag from this PR, though I'm not sure we should touch pp.analyze right now.

If it's something you want to try working on, and you are OK with your work potentially being discarded, feel free to go ahead. I just wrote up some ideas for how to do it intelligently, but I deleted them because it's unclear whether it would actually work. Probably the simplest for now would be to make pp.analyze tag all coercions with this new pp.coercions.types flag.

[tonyxty]

I changed the new option to default to false. It makes sense for two reasons: compatibility with current tests, and looking disruptive in the infoview.

If it's something you want to try working on

It seems to me that it belongs to a separate PR. Shall we discuss how to proceed on Zulip before I start working on pp.analyze?

[kmill]

Could you please add some tests? How about in tests/lean/run/coeAttr.lean, and use module docstrings like in lean/run/conv_arg.lean to say what each test is trying to accomplish. Two tests, one with the option false and one with the option true, should be sufficient.

[tonyxty]

I've added some very basic tests.