Zulip Chat Archive

Stream: general

Topic: parser issue with `]`


view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:59):

I think the 0 at the end matters right

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 14:16):

apparently


Last updated: May 09 2021 at 18:17 UTC