## Stream: general

### Topic: parser issue with ]

#### Kevin Buzzard (Aug 17 2020 at 13:56):

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 (Aug 17 2020 at 13:58):

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 (Aug 17 2020 at 13:59):

I think the 0 at the end matters right

#### Kevin Buzzard (Aug 17 2020 at 14:16):

apparently

Last updated: May 09 2021 at 18:17 UTC