diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 38ef1c387..ecc5b9208 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -29,7 +29,7 @@ reserve prefix `¬`:40 reserve prefix `~`:40 reserve infixr `∧`:35 reserve infixr `/\`:35 -reserve infixr `‌\/`:30 +reserve infixr `\/`:30 reserve infixr `∨`:30 reserve infix `<->`:25 reserve infix `↔`:25