Pretty printing `proofs.WithType`

Stream: mathlib4

[Oliver Nash]

If we add:

  "-Dpp.proofs.withType=false",

to Mathlib's lakefile.lean here, will that mean that Mathlib behaves as though I've typed:

set_option pp.proofs.withType false

at the top of any file on which I'm working?

[Oliver Nash]

If so, would others support this change?

[Sky Wilshaw]

I'm not working on mathlib, but I've ended up putting that at the top of pretty much every file I use in my project.

[Oliver Nash]

I've proposed this in #7211