Pretty-printing of proof arguments

Stream: mathlib4

[Michael Rothgang]

A question came up in #10082: should an argument like (s : Opens X) the above be made implicit, if there's a named hypothesis from which s can be inferred? My understanding is that in principle, we like that change - but @Yury G. Kudryashov pointed out:

The reason why we kept these arguments explicit in Lean 3 was the following: if you have myDef {x : α} (hx : MyProp x) and the proof of hx is nontrivial (not just a variable), then Lean pretty prints it as myDef _.

Does anybody know if this is was fixed with Lean 4 (e.g., by printing the type of hx in this case)?
(If not, I agree the PR should be closed.)

[Joachim Breitner]

The printing of proofs is controlled using the pp.proofs options, so if you ask Lean nicely, it will print the proofs in full glory.

[Kyle Miller]

In particular, pp.proofs (default: false) controls whether to pretty print proofs or to elide them, and if false, then pp.proofs.withType (default: true) controls whether to add a type ascription, so whether to pretty print as (_ : MyProp x) rather than just _.

[Winston Yin (尹維晨)]

This option is not very discoverable to the user, but I find it a bit strange to make an argument explicit just because of pretty printing. Perhaps it is enough to see the type of _ when you click on it.

[Michael Rothgang]

Thanks for the insight. Given these, I propose to move forward with the PR.
(This option being hard to discover is a separate issue, which I would prefer to address indepedently.)

[Eric Wieser]

Winston Yin (尹維晨) said:

This option is not very discoverable to the user, but I find it a bit strange to make an argument explicit just because of pretty printing. Perhaps it is enough to see the type of _ when you click on it.

Note that it's possible to write a custom delaborator for your function so that the argument is visible in the pretty printer by default, even if it's implicit (or to show the type for a proof even if it's disabled)

[Eric Wieser]

You can't click on _ in the web docs

[Kyle Miller]

In the next Lean release, there's now an option to make deep terms pretty print as ⋯. It has features such as (1) hovering over ⋯ in the infoview shows the pretty printed term, not the @ explicit form and (2) if you copy/paste it from the infoview, it throws an elaboration error letting you know what pretty printer option caused it.

We probably should make pp.proofs use ⋯ too, which would give a better UX than _.

[Kyle Miller]

Would anyone find this to be an upgrade to how the pp.proofs feature omits proofs?

[Kyle Miller]

lean4#3241 is an exploration of this

It also gives a pp.proofs.threshold option to let some more complicated terms get pretty printed. I've set the default value to 0, which means "pretty print only atomic proofs, like constants and local variables", which how pp.proofs works right now.