notation not used in infoview

Stream: general

[Patrick Massot]

In the following, does anyone understand why Lean uses the notation in the second example but not in the first one?

import algebra.big_operators

open finset

notation `∑` binders ` to ` n `, ` r:(scoped:67 f, ((finset.range n).sum  f)) := r

example (n : ℕ) : ∑ i to n, i = (n * (n - 1)) / 2 :=
begin
/-
n : ℕ
⊢ (range n).sum (λ (i : ℕ), i) = n * (n - 1) / 2
-/
sorry
end

notation `∑` binders ` in ` s `, ` r:(scoped:67 f, (finset.sum s f)) := r

example (n : ℕ) : ∑ i in range n, i = (n * (n - 1)) / 2 :=
begin
/-
n : ℕ
⊢ ∑ (i : ℕ) in range n, i = n * (n - 1) / 2
-/
sorry
end

[Patrick Massot]

@Sebastian Ullrich maybe?

[Eric Wieser]

I think the notation has to be associated to a single definition in order to be used by the pretty printer? Does it work if you introduce a sum_range definition?

[Sebastien Gouezel]

It's fine if you use

notation `∑` binders ` to ` n `, ` r:(scoped:67 f, (finset.sum (finset.range n) f)) := r

If I remember correctly, using dot notation in a notation has problems.

[Patrick Massot]

Thanks a lot Sébastien!