(⨁ i, Mᵢ i) →+ M parsing

Stream: maths

[Kevin Buzzard]

The bracketless ⨁ i, Mᵢ i →+ M looks ok to me, but Lean wants (⨁ i, Mᵢ i) →+ M. Am I naive in thinking that trying to remove the brackets by fiddling with priorities would be a good idea? I don't really know enough about parsing to do this though :-/ It's all the binders, scoped stuff I still feel a bit intimidated by.

import algebra.direct_sum

open_locale direct_sum

#print notation →+ -- _ `→+`:25 _:24 := add_monoid_hom #1 #0
#print notation ⨁ -- `⨁`:1024 binders `,`:0 (scoped 0) := #0

variables (ι : Type) (Mᵢ : ι → Type) [∀ (i : ι), add_comm_monoid (Mᵢ i)]
variables (A : Type) [add_comm_monoid A]

#check ⨁ i, Mᵢ i →+ A -- parses but becomes the sum of the maps, not the map from the sum

[Eric Wieser]

I think it's probably a bad idea; the current binding power matches that of \Pi and \Pi\0, so we'd need a good argument for why direct_sum is different.