line break in tactic.pp

Stream: Is there code for X?

[Frédéric Le Roux]

I use tactic.pp inside a tactic, and Lean introduces a line break in the middle of the expression
(specifically, I get

(f⁻¹⟮(⋂ (i : I), F i)⟯ ⊆ ⋂ (i : I), f⁻¹⟮F i⟯) ∧
  f⁻¹⟮(⋂ (i : I), F i)⟯ ⊆ ⋂ (i : I), f⁻¹⟮F i⟯

with the line break after the ∧).
Is there a way to avoid this? I see there is a parameter pp_widthbut I do not know how to set it inside a tactic (and thus I do not know if this is the right parameter to handle this issue).

[Scott Morrison]

Can you use set_option pp.width 1000? (Before the declaration.)

[Frédéric Le Roux]

I tried this before the meta def, or before the use of it, but it has no effect.
Is there a way to set this option inside the meta def?

[Gabriel Ebner]

docs#tactic.pp produces a docs#format object. The line width is only relevant when converting a docs#format object to docs#string. That's where the pp.width option needs to be set. The docs#format.to_string function has an optional docs#options argument. Try setting it there using docs#options.set_nat .

[Frédéric Le Roux]

I am unable to find a place showing the usage of options.set_nat. I naively tried options.set_nat pp.width 1000, but that does not work.