lean 3/4 bool ! precedence

Stream: mathlib4

[Kevin Buzzard]

In mathlib3 we have

prefix `!`:90 := bnot

In core Lean 4 we have

@[inheritDoc] notation:max "!" b:40 => not b

and as a result the following works in Lean 3:

import data.bool.basic -- just for ! notation

lemma bnot_not_eq : ∀ {a b : bool}, ¬!a = b ↔ a = b := sorry (`dec_trivial` works)

lemma bnot_ne {a b : bool} : !a ≠ b ↔ a = b := bnot_not_eq

but in Lean 4 this doesn't work

import Init.Notation -- for ! notation

theorem bnot_not_eq : ∀ {a b : Bool}, ¬!a = b ↔ a = b := sorry

theorem bnot_ne {a b : Bool} : !a ≠ b ↔ a = b := bnot_not_eq -- fails
/-
type mismatch
  bnot_not_eq
has type
  ¬(!decide (?m.238 = ?m.239)) = true ↔ ?m.238 = ?m.239 : Prop
but is expected to have type
  (!decide (a ≠ b)) = true ↔ a = b : Prop
-/

because things are being parsed differently. What do I do?

[Mario Carneiro]

mathport should be inserting parentheses as necessary to make the definition work out with the new precedences. You should also put in parentheses where necessary to make the statement equivalent to the lean 3 version

[Mario Carneiro]

although if you think the precedence change is in error you could also open an issue on lean 4