Define own notation

Stream: general

[Jujian Zhang]

Sometimes an additive group can be module of different rings, to differentiate the different scalar multiplication I want to introduce notations for different module instances. But since the "type" of the new notation is still has_smul.smul, in goal view Lean will always still show the same •, is there a way to ask Lean prioritizing which notation to use?

An mwe:

import algebra

variables {R S : Type} [ring R] [ring S] (f : R →+* S)
variables (M : Type) [add_comm_monoid M] [module S M]
local notation r `•[f]` := @@has_smul.smul (module.comp_hom _ f).to_has_smul r

example (r : R) (m : M) : r •[f] m = m :=
begin
  -- goal shows r • m = m
  -- but I want it to show r •[f] m = m
  change (r •[f] m) = m,
  -- goal still shows r • m = m
  sorry
end

So I can write scalar multiplication using customized notation, but I cann't read customized notation in goal view

[Johan Commelin]

@Jujian Zhang The recommended way is to use docs#is_scalar_tower

[Eric Wieser]

I think the actual problem here is that lean won't ever pretty print notation with a @ in its definition; not that it's choosing the existing notation over your notation.

[Eric Wieser]

Of course, the notation f r • m works just fine ;)

[Jujian Zhang]

@Eric Wieser but this silly example without @doesn't work either

import algebra

notation r `••` := has_smul.smul r

example : 0 •• 1 = 2 :=
begin
  -- goal shows 0 • 1 = 2
  -- but I want it to show 0 •• 1 = 2
  change (0 •• 1) = 2,
  -- goal still shows 0 • 1 = 2
  sorry
end

[Eric Wieser]

It works as notation r `••` x := has_smul.smul r x

[Eric Wieser]

In this example, I think lean prefers notation for large expressions over notation for subexpressions

[Eric Wieser]

See:

constant foo : ℕ → ℕ → ℕ → ℕ

-- reordering has no effect
notation `F3` := foo _ _ _
notation `F2` := foo _ _
notation `F1` := foo _

#check foo 1  -- F1
#check foo 1 2  -- F2
#check foo 1 2 3  -- F3

for proof of that