From 5b2b2d8069a07b064ff2d3da0c96f1caeff9374a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 1 Dec 2020 14:00:39 +0100 Subject: [PATCH] chore: declare ASCII notations first --- src/Init/Notation.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index abf6630206..04fa7a063c 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -21,21 +21,22 @@ infixl:70 " % " => Mod.mod infixl:70 " %ₙ " => ModN.modn infixr:80 " ^ " => Pow.pow -infix:50 " ≤ " => HasLessEq.LessEq +-- declare ASCII alternatives first so that the latter Unicode unexpander wins infix:50 " <= " => HasLessEq.LessEq +infix:50 " ≤ " => HasLessEq.LessEq infix:50 " < " => HasLess.Less -infix:50 " ≥ " => GreaterEq infix:50 " >= " => GreaterEq +infix:50 " ≥ " => GreaterEq infix:50 " > " => Greater infix:50 " = " => Eq infix:50 " == " => BEq.beq infix:50 " ~= " => HEq infix:50 " ≅ " => HEq -infixr:35 " ∧ " => And infixr:35 " /\\ " => And -infixr:30 " ∨ " => Or +infixr:35 " ∧ " => And infixr:30 " \\/ " => Or +infixr:30 " ∨ " => Or infixl:35 " && " => and infixl:30 " || " => or