Printing of multiple optional argument

[fonqL]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

A small pretty printer bug in multiple optional argument.

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

#check f 0

shows f 0 1 2 : Nat instead of f 0 : Nat or f 0 1 2 3 : Nat. The last optional argument is missing.

Context

Zulip

Discover this bug when using Array.foldl.

Versions

4.9.0

Additional Information

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.