leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: Creating my own pp.all = true string


Jason Rute (Feb 07 2020 at 23:45):

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 (Feb 08 2020 at 00:08):

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

Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll