parser issue with `]`

Stream: general

[Kevin Buzzard]

import tactic

-- rolling our own left action

/-- A left action of some group `G` on some `S` is a function with type
  `to_fun : G → S → S` such that for all `s : S`, `to_fun 1 s = 1` and for all
  `g, h : G`, `s : S`, `to_fun g (to_fun h s) = to_fun (g * h) s` -/
structure laction (G : Type) [group G] (S : Type) :=
(to_fun    : G → S → S) (map_one' : ∀ s : S, to_fun 1 s = s)
(map_assoc' : ∀ g h : G, ∀ s : S, to_fun g (to_fun h s) = to_fun (g * h) s)

variables {G S : Type} [group G]
variables {μ : laction G S}

-- note the below line appears in mathlib

-- notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := linear_map R M M₂

-- and this surely is pretty much the same, right?

notation g ` ★[ `:70 μ ` ] `:70 s := μ.to_fun g s

variable {H : Type}

-- now uncomment the below line for a timeout

-- variable [group H]

[Kevin Buzzard]

o_O I can just fix it by changing the binding power numbers to match the mathlib notation. I don't know what's going on but at least I can now proceed.

[Kenny Lau]

I think the 0 at the end matters right

[Kevin Buzzard]

apparently