pp_extended_field_notation and Quiver.Hom.op

Stream: mathlib4

[Kevin Buzzard]

Lean 3 (nonempty.some h₁).map.op is being pretty-printed as (Quiver.Hom.op (Nonempty.some h₁).map) in Lean 4, so I tried to fix this with pp_extended_field_notation Quiver.Hom.op but this gives me the error Quiver.Hom is not a structure. The other method I understand,

@[app_unexpander Quiver.Hom.op] def
  unexpandQuiver.Hom.op : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).op $(X)*)
  | _                 => throw ()

seems to work fine. Should I be adding this app_unexpander? (again I'm debugging large terms and trying to compare manually)

[Kyle Miller]

No, pp_extended_field_notation should work for this. It has a check For Your Own Good that the namespace corresponds to a structure, but this isn't strictly speaking needed: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ProjectionNotation.lean#L130-L131

[Kyle Miller]

If that check fails, then this case shouldn't be there

[Kyle Miller]

@Kevin Buzzard mathlib4#3946