dot notation in infoview

Stream: lean4

[Ben Selfridge]

Any way to completely disable dot notation pretty-printing in infoview?

[Kyle Miller]

set_option pp.fieldNotation false

[Ben Selfridge]

Awesome -- any idea how I can find these things out by myself in the future? Google doesn't seem to work very well for stuff like this.

[Kyle Miller]

The #help option pp command shows you all the options (if you have the right Batteries modules imported). Eventually this should appear in the reference manual too.

I looked at https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Options.lean, since I happen to have the Lean source code open.

[Asei Inoue]

you can see https://seasawher.github.io/mathlib4-help/options/