Postfix + dot notation

Stream: lean4

[Peter Nelson]

Is there a way to define a postfix operator that binds more strongly than dot notation? I would like to do something like the following without the need for parentheses around the n*.

import Mathlib.Data.Nat.Basic

def add_five : ℕ → ℕ := fun x ↦ x+5

postfix:max "*" => add_five

lemma star_succ (n : ℕ) : (n*).succ = n.succ* := by
  simp [add_five]

-- lemma star_succ' (n : ℕ) : n*.succ = n.succ* := by sorry
-- breaks without parentheses

[Kyle Miller]

It seems that the problem is an ambiguity in n*.succ, since it could mean n * .succ, since .succ is valid syntax.

This works fine:

postfix:max "**" => add_five

lemma star_succ (n : ℕ) : n**.succ = n.succ** := by
  simp [add_five]

[Peter Nelson]

Thanks!