What does format.width do?

Stream: lean4

[Eric Wieser]

I was expecting

set_option format.width 10

example (x : Nat) : x * 30 ≠ 0 := by
  repeat rw [Nat.mul_succ]
  sorry

to affect the output width, but it seems that the 10 is ignored. In lean3, it works as expected:

set_option pp.width 10

example (x : nat) : x * 30 ≠ 0 := by
  repeat { rw [nat.mul_succ] }; sorry

[Eric Wieser]

The docstring for the setting is just the word "indent"