lean#691

Stream: PR reviews

[Kyle Miller]

This is a Lean PR to get the pretty printer to display the types of numerals as type ascriptions when you either add an attribute or set a pretty printer option:

attribute [pp_numeral_type] fin
#check (2 : fin 17) + 3
-- (2 : fin 17) + (3 : fin 17) : fin 17

set_option pp.numeral_types true
#check (2 : fin 17) + 3
-- (2 : fin (17 : ℕ)) + (3 : fin (17 : ℕ)) : fin (17 : ℕ)

There are two use cases I'm imagining: (1) sometimes you aren't sure whether 2 ^ 2 has a nat or a real exponent, so the option can help you debug without having to turn numerals off completely, and (2) with types like zmod you might rather have it always display ascriptions for numerals (for teaching, for example), since (2 : zmod 5) = (7 : zmod 5) in this situation is better than seeing just 2 = 7.

Are there any other use cases that this might be useful for? Any additional configurable options that might be needed to support them?

[Kyle Miller]

(Ideally it could be context-aware and insert ascriptions only where the types are ambiguous, but that seems like it would be a much larger project!)

[Patrick Massot]

This is a very nice idea, especially for teaching. I hope Lean 4 will have this as well (in one way or another, I guess it doesn't have to be in core).

[Eric Wieser]

I'm not sure I understand why you would ever _not_ want to put the pp_numeral_type attribute on something

[Eric Wieser]

Unless the idea is that we put it on nothing, and you only attach it to things when debugging

[Eric Wieser]

Either way, this is a great change!

[Mario Carneiro]

I think the default should still be nothing

[Mario Carneiro]

If you are looking at a proof term or a norm_num proof or other larger term with a lot of numbers the type ascriptions will blow up the term by 5x

[Mario Carneiro]

it seems appropriate as something you turn on when you want more information like pp.universes

[Yaël Dillies]

Yes. Bhavik and I had quite a few very calculatory proofs in SRL and I really don't need this option to reach unreadable tactic states (and everything is in ℕ or ℚ anyway). Setting it on occasionally for debugging sounds great however!

[Gabriel Ebner]

The option is great (and easy to implement in Lean 4), but I agree with Mario that it definitely shouldn't be the default.