Option to show user names in non-dependent binders

[Vtec234]

trafficstars

Description

There does not seem to be a pp option which would make the delaborator put in names of non-dependent binders when they do not contain macro scopes (so when they are written by a user). If there is this option, apologies, I couldn't find it! I think showing these might be desirable since inductive argument names are often meaningful, so it may even be sensible to enable this by default.

For example:

inductive Foo where
  | a : (n : Nat) → Foo
  | b (n : Nat) 

set_option pp.all true
/- Foo.a : Nat → Foo -/
#check @Foo.a
/- Foo.b : Nat → Foo -/
#check @Foo.b

Expected behavior: Foo.a : (n : Nat) → Foo and similarly Foo.b : (n : Nat) → Foo are shown when some pp option is set.

Actual behavior: Foo.a : Nat → Foo is shown.

Reproduces how often: 100%

Versions

09e4c00c681a6e4fd822bd5a5c213af943a8c009

[leodemoura]

We have the following open issue https://github.com/leanprover/lean4/issues/375 Do you see the new flag being useful for nested binders too? I am asking because if its main application is for signatures, I suggest we close this issue and focus on #375. What do you think?

[Vtec234]

The main application I had in mind for this is to delaborate constructors. That is, in a procedural macro I wanted to transform Foo into something like

inductive FooBar
  | aBar : (n : Nat) → FooBar
  | bBar : (n : Nat) → FooBar

It is important that the user names are preserved here. I think the signature printer could work for that by instead producing

inductive FooBar
  | aBar (n : Nat)
  | bBar (n : Nat)

with some complications such as needing to print just aBar instead of FooBar.aBar. If you agree, please feel free to close this.

[leodemoura]

@Kha What do you think?

[Kha]

I believe we want to have pp.all roundtrip as much as possible, so it would make sense that it should preserve binder names. If we want that, we may as well introduce a dedicated option for it instead of having "hidden" pp.all behavior.