Printing of multiple optional argument

Stream: general

[fonqL]

def f (a: Nat) (b := 1) (c := 2) (d := 3) := a + b + c + d

#check f 0    -- f 0 1 2 : Nat

It's a bit strange.
My expected behavior is f 0 or f 0 1 2 3.

[Julian Berman]

That does seem strange, I think that would be a small Repr bug? And probably worth filing on the Lean 4 repo.

[fonqL]

4812

[Yaël Dillies]

You can type lean4#4812 and Zulip will display it as lean4#4812

[Matthew Ballard]

Or just lean#4812

[fonqL]

Oh thanks. I used to think that lean4#num was pointing to a PR and I just find that issues and PRs share the same serial number. :exploding_head:

[Kyle Miller]

Thanks for reporting it. It's a known (but until-now unreported) issue, where the algorithm for pretty printing optional arguments only considers omitting the last optional argument here.

Fixing this is low-priority, but getting :+1:'s on that issue could help motivate putting effort into improving the pretty printing.

[Kyle Miller]

(By the way @Julian Berman, the Repr typeclass is not used for expression pretty printing, like what #check does — one way you can tell the difference is whether expressions in the output have hovering information. Repr is used by #eval though.)

[Julian Berman]

Aha, interesting, thanks for the correction.