Stream: Is there code for X?
Topic: line break in tactic.pp
Frédéric Le Roux (Aug 26 2020 at 08:25):
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
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