Zulip Chat Archive

Stream: Is there code for X?

Topic: line break in tactic.pp


view this post on Zulip 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).

view this post on Zulip Scott Morrison (Aug 26 2020 at 10:24):

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

view this post on Zulip 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?

view this post on Zulip 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 .

view this post on Zulip 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