attribute [pp_dot]

Stream: general

[Martin Dvořák]

What is the Lean 4.18's equivalent of Lean 4.2's attribute [pp_dot] please?

[Yaël Dillies]

No attribute. pp_dot is now the default

[Martin Dvořák]

example (l : List α) (f : α → α) : l.map f = l.map f := by
  rfl

Infoview shows:

List.map f l = List.map f l

How can I make it display what I wrote please?

[Aaron Liu]

pretty printer uses dot notation if the first explicit argument has the correct type matching the namespace of the function

[Martin Dvořák]

Oh, I forgot. So, custom delaborator is the only option here?

[Martin Dvořák]

For future visitors:
https://github.com/madvorak/chomsky/commit/11b9fa414e7e1b8f08155a4a83072a5bd6b6f882