delaborator for Finset.sun does not trigger

Stream: mathlib4

[Jon Eugster]

In the following MWE the second sum does not get pretty-printed the way I'd like it too:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Matrix.Basic

open BigOperators

/-- Test that the delaborator works in this particular case. -/
example (n : Nat) (r s : Fin n) :
    ∑ i : Fin n, (1 : Matrix (Fin n) (Fin n) Nat) r s =
    (∑ i : Fin n, (1 : Matrix (Fin n) (Fin n) Nat)) r s := by
  -- check pretty-printing here
  simp

this gets displayed as

∑ i : Fin n, 1 r s = Finset.sum Finset.univ (fun i => 1) r s

I would like to see

∑ i : Fin n, 1 r s = (∑ i : Fin n, 1) r s

The reason is that the delaborator assumes that Finset.sum has exactly 5 Arguments in this line of the source code but in my example with matrices, there are 7 arguments. I tried to modify the delaborator but there are two things I don't understand:

• At the place where it calls ← delab is there a way to tell it to only delab using the first 5 arguments and ignoring any more arguments?
• If I do a match case for additional arguments, I end up with an args : Array Expr containing all arguments that aren't really part of the sum, and I just want to print them at the end of the pretty-printed Syntax. How would I have to modify the snippets `(∑ $binder, $body) ? Something similar to `((∑ $binder, $body)) $args? Except that $args seems not to be the right thing.

[Eric Wieser]

I think lean4#3375 is supposed to have fixed this?

[Kyle Miller]

That Lean PR won't fix this one. You can put the withOverApp combinator around that delaborator to get it to handle over-application.

[Kyle Miller]

Here's fixing delabFinsetProd, and delabFinsetSum is similar:

@[scoped delab app.Finset.prod] def delabFinsetProd : Delab :=
  whenPPOption getPPNotation <| withOverApp 5 do
  let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
  guard <| f.isLambda
  let ppDomain ← getPPOption getPPPiBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    return (i, ← delab)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ←
      if ppDomain then
        let ty ← withNaryArg 0 delab
        `(extBinder| $(.mk i):ident : $ty)
      else
        `(extBinder| $(.mk i):ident)
    `(∏ $binder, $body)
  else
    let ss ← withNaryArg 3 <| delab
    `(∏ $(.mk i):ident in $ss, $body)

[Eric Wieser]

Ah, I was looking for withOverApp but could not find it

[Eric Wieser]

Pretty much every delab app. should use withOverApp, right?

[Eric Wieser]

I'll make a PR

[Eric Wieser]

#12022

[Jon Eugster]

Thank you very much, both of you!