shadowing prelude operations

Stream: general

[Thorsten Altenkirch]

For my logic course I would like to redefine some operations from the prelude for pedagogical reasons (! , & , |, * , +). This worked in lean 3 but seems to cause problems in lean 4.

E.g. I write

local prefix:90 "!" => not
local infixl:50 " && " => and
local infixl:40 " || " => or

but when I use them I get an ambigious term error:

theorem b_dm2 : ∀ b c : Bool,
   (! (b && c)) = (!b || ! c) := by sorry

Is there a straightforward way to fix that?

[Floris van Doorn]

local prefix:90 (priority := high) "!" => not
local infixl:50 (priority := high) " && " => and
local infixl:40 (priority := high) " || " => or