local notation

Stream: new members

[Yannick Seurin]

What's the best way to introduce some kind of "local notation", e.g., say I want to prove things about a finite group $G$ of order $n$. Here $n$ is really just a shorthand to avoid typing Fintype.card G every time.

I tried

import Mathlib

variable (G : Type) [Group G] [Fintype G]
         (n : ℕ) (G_card_n : Fintype.card G = n)

include G_card_n
-- start proving theorems

But practicing a bit, it does not seem very convenient (one ends up invoking G_card_n at the start of each proof to replace n). I guess what I have in mind would be some kind of macro that would be replaced by Fintype.card G before building. It seems that Lean3 had a local notation command that worked this way (as far as I understand) but that has apparently been removed.

[Eric Wieser]

If you write open Fintype (card), then you can use card G which is much shorter than Fintype.card G

[Ruben Van de Velde]

Also, what makes you say local notation is removed? I see hundreds of uses in mathlib

[Yannick Seurin]

Maybe syntax has changed but

local notation `n` := Fintype.card G

does not seem to work in vscode

[Yannick Seurin]

I get

unexpected token '`'; expected '=>'

[Yannick Seurin]

OK, found the correct new syntax

local notation "n" => Fintype.card G