## Stream: Is there code for X?

### Topic: line break in tactic.pp

#### Frédéric Le Roux (Aug 26 2020 at 08:25):

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 (Aug 26 2020 at 10:24):

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

#### Frédéric Le Roux (Aug 26 2020 at 11:31):

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 (Aug 26 2020 at 11:42):

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 (Aug 26 2020 at 12:25):

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.

Last updated: May 19 2021 at 02:10 UTC