pretty printer in to_string

Stream: general

[Frédéric Le Roux]

When using to_string expr in metaprograming, is there a way to force Lean to use the pretty printer?
I would like to get the target into a string in pretty printed format.

[Patrick Massot]

You can use tactic.pp

[Patrick Massot]

Very stupid example:

meta def fred : tactic unit :=
do h ← tactic.get_local `h >>= tactic.pp,
  tactic.trace h

example (h : 0 = 1) : false :=
begin
  fred,
  tauto,
end

[Patrick Massot]

In case you're still afraid of monadic combinators, you can avoid the >>= by using:

do h ← tactic.get_local `h,
   print ← tactic.pp h,
   tactic.trace print

[Frédéric Le Roux]

Thanks!