lean#692

Stream: PR reviews

[Kyle Miller]

With lean#691, I'd decided what to do about unary nats (nat constructor expressions) as an afterthought, but admittedly it was nonintuitive and could lead to confusion.

This PR modifies it to do things the right way, I hope. There's now an option (pp.nat_numerals) to control whether these expressions get represented as numerals, and then they are processed in exactly the same way as other numerals.

attribute [pp_numeral_type] nat
#check 3
#check nat.zero.succ.succ.succ
-- both give (3 : ℕ) : ℕ

set_option pp.nat_numerals false
#check nat.zero.succ.succ.succ
-- (1 : ℕ).succ.succ : ℕ

set_option pp.numerals false
set_option pp.nat_numerals true
#check nat.zero.succ.succ.succ
-- nat.zero.succ.succ.succ : ℕ

There was a vestigial internal option that controlled this anyway, and this new pp.nat_numerals exposes it. I've set it to be contingent on pp.numerals being true, for principle of least surprise.

[Kyle Miller]

I'm planning on creating some mathlib documentation listing all the pp options, so we don't have to dig up and pass around links to Zulip messages with the useful ones.

[Kyle Miller]

There is a bit of a bug, which is that when this option is false the expressions fail to round-trip:

set_option pp.nat_numerals false

#check nat.zero.succ.succ.succ
-- 1.succ.succ : ℕ

#check 1.succ.succ
-- invalid field notation, type is not of the form (C ...) where C is a constant

However, with an additional option it works:

set_option pp.nat_numerals false
set_option pp.numeral_types true

#check nat.zero.succ.succ.succ
-- (1 : ℕ).succ.succ : ℕ

#check (1 : ℕ).succ.succ
-- (1 : ℕ).succ.succ : ℕ

I'm not sure if there's any good way to fix this.