do I need a delaborator?

Stream: mathlib4

[Kevin Buzzard]

I'm getting LinearMap.comp (map φ ψ) comul in the infoview. Can I make it say (map φ ψ).comp comul instead?

[Kevin Buzzard]

I got as far as this

attribute [pp_dot] LinearMap.comp
/-
unknown declaration '_aux_scratch___LinearMap_comp_unexpander_1'
-/

[Kyle Miller]

#mwe? I don't see any error.

[Kevin Buzzard]

no you're right, I can't reproduce :-) Thanks!

[Kevin Buzzard]

Should I add

attribute [pp_dot] LinearMap.comp
attribute [pp_dot] LinearMap.mul'

to mathlib?

[Patrick Massot]

I think we really need to make this the default, just as it was in Lean 3.

[Kevin Buzzard]

I have since discovered ∘ₗ and am now confused about what the simp normal form is.

[Adam Topaz]

is that not notation for LinearMap.comp?

[Kevin Buzzard]

If it's notation then I'm surprised I was seeing comp at all?

[Yaël Dillies]

Well it depends whether it's delaborated notation or input-only notation

[Kevin Buzzard]

I have no idea what this means

[Yaël Dillies]

I'm asking you whether ∘ₗ has a delaborator, assuming that by "I was seeing comp" you mean "I was seeing comp in the infoview".

[Kyle Miller]

Yes, it does have one. It's generated by notation3. https://github.com/leanprover-community/mathlib4/blob/89f9777575aaa0e4190c64c8247b03f7864f67e8/Mathlib/Algebra/Module/LinearMap.lean#L575

Unfortunately, the delaborators it generates can be very very sensitive. For example, notation3's delaborators only handle matching expressions sort of syntactically. If there are instance arguments, it doesn't know how to do those checks up to defeq.

This should be improvable, but perhaps (1) the notation command itself could get these improvements and/or (2) notation3 could be replaced by a new mathlib 4 notation command, since notation3 is after all meant to ease the port of Lean 3 notations -- the delaborator generator made it achieve feature parity with Lean 3's notation command.

[Floris van Doorn]

I've also noticed places where, when applying some notation to an extra argument ((L ∘ₗ L') x instead of L ∘ₗ L') causes the delaborator to not work.

[Kyle Miller]

Overapplication is a common issue with pretty printers. The fundamental issue is that you have to know how many arguments are part of the notation, and how many are additional arguments. The notation command doesn't have much hope of solving it directly, but notation3 could.

Unhandled overapplication is something that's on my radar for things to fix in the delaborator. In the next Lean release we'll see this fixed for overapplied structure projections (so there will be no need for pp_dot on Prefunctor.obj and Prefunctor.map for example).