pp.analyze for summation notation

Stream: mathlib4

[Jakub Nowak]

With pp.analyze true the output of delaboration doesn't survive round-trip. Can we improve this?

import Mathlib

set_option pp.analyze true in
example : ∑ (i : Fin 3), i.val = 3 := by
  -- ⊢ ∑ i, ↑i = 3
  have : ∑ i, ↑i = 3 := by decide

The problem was found here: #new members > `rewrite` doesn't match in a seemingly matching goal

[Jakub Nowak]

Hmm, I've tried using trace or logInfo in Delab function, but neither seem to work (they compile, but there's no output in infoview). Does anyone know of a way to add debug logging to Delab function?

[Eric Wieser]

You can use dbgTrace I think

[Jakub Nowak]

Eric Wieser said:

You can use dbgTrace I think

Doesn't work either.

[Jakub Nowak]

Ah, no, sorry, it works! I've accidentally edited Finset.prod instead of Finset.sum.

[Jakub Nowak]

#33070