Pretty printing applied function composition

[PatrickMassot]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The delaborator doesn't use the function composition notation when the composition is applied.

Steps to Reproduce

variable (f : α → β) (g : β → γ) (x : α)

#check (g ∘ f) x

Expected behavior: [What you expect to happen]

See (g ∘ f) x : γ.

Actual behavior: [What actually happens]

See Function.comp g f x : γ.

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

leanprover/lean4:nightly-2023-01-17 under Linux.

See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Function.2Ecomp.20pretty.20printing

[djvelleman]

This particular problem can be fixed with an unexpender:

@[app_unexpander Function.comp] def unexpandFunctionComp : Lean.PrettyPrinter.Unexpander
  | `($(_) $f:term $g:term $x:term) => `(($f ∘ $g) $x)
  | _ => throw ()

However, Mario Carneiro reports in the Zulip discussion referenced above that a more general fix is in the works.