Zulip Chat Archive

Stream: mathlib4

Topic: lean 3/4 bool ! precedence


Kevin Buzzard (Oct 21 2022 at 17:14):

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 (Oct 21 2022 at 20:52):

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 (Oct 21 2022 at 20:53):

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


Last updated: Dec 20 2023 at 11:08 UTC