Difference in precedence between unicode ¬ and ascii Not

Stream: lean4

[Spearman]

I ran into a difference in precedence between the unicode ¬ and the ascii equivalent 'Not'

In the barber example of chapter 4 of Theorem Proving in Lean 4 https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html:

variable (men : Type) (barber : men)
variable (shaves : men -> men -> Prop)
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := sorry
example (h : forall x : men, shaves barber x <-> Not shaves x x) : False := sorry

replacing ¬ with Not results in the error

warning: ././././Main.lean:5:0: declaration uses 'sorry'
error: ././././Main.lean:6:53: application type mismatch
  ¬shaves
argument
  shaves
has type
  men → men → Prop : Type
but is expected to have type
  Prop : Type
error: Lean exited with code 1
Some builds logged failures:
- Main
error: build failed

It needs to have parentheses around shaves x x:

example (h : forall x : men, shaves barber x <-> Not (shaves x x)) : False := sorry

Are there other unicode symbols that have different binding precedence than their ascii equivalents?

[Mario Carneiro]

Not is not really an "ascii equivalent" of the symbol ¬, it's the underlying name of the notation

[Mario Carneiro]

it follows the normal precedence rules of applications

[Kevin Buzzard]

Notation has a rich variety of precedences, function application always has the same precedence.