Zulip Chat Archive

Stream: general

Topic: printing inferred quantities and `pp.all`


Gihan Marasingha (Jul 16 2021 at 09:53):

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 (Jul 16 2021 at 10:12):

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

Gihan Marasingha (Jul 16 2021 at 10:48):

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

Last updated: Dec 20 2023 at 11:08 UTC