printing inferred quantities and `pp.all`

Stream: general

[Gihan Marasingha]

In the following, I can get Lean to print the inferred predicate through set_option pp.all true.

lemma foo (s t u : ℕ) : s + (t + u) = s + (u + t) := eq.subst (nat.add_comm t u) rfl

set_option pp.all true

#print foo

Is there a way to do this that doesn't disable use of notation?

Follow-up / related question. The pp.all documentation states that it "display coercions, implicit parameters, proof terms, fully qualified names, universes, and disable beta reduction and notation during pretty printing".

I tried to simulate this using the following options:

set_option pp.coercions true
set_option pp.implicit true
set_option pp.proofs true
set_option pp.full_names true
set_option pp.universes true
set_option pp.beta false
set_option pp.notation false

But these don't suffice to print the predicate in the proof of foo. What is the difference between pp.all true and the above?

[Eric Wieser]

I think you can always set pp.all then turn some settings back to normal afterwards

[Gihan Marasingha]

Thanks. Doing the following enables notation, but it also disables the pretty printing of the predicate.

lemma foo (s t u : ℕ) : s + (t + u) = s + (u + t) := eq.subst (nat.add_comm t u) rfl

set_option pp.all true
set_option pp.notation true

#print foo