feat: display coercions with a type ascription

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 428 forks source link

feat: display coercions with a type ascription #6119

Closed tonyxty closed 1 week ago

tonyxty commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

I've added some very basic tests.