Creating my own pp.all = true string

Stream: general

[Jason Rute]

Inside a tactic I want to generate a string of an expression with the same format as when the option pp.all is set to true. How do I do that?

[Mario Carneiro]

run_cmd do
  let e := `(∀ n : ℕ, n = n),
  tactic.set_options (options.mk.set_bool `pp.all tt),
  tactic.pp e >>= tactic.trace
  -- ∀ (n : nat), @eq.{1} nat n n