max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: declare ASCII notations first

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-01 14:00:39 +01:00 • committed by Leonardo de Moura
parent 1f9e8bc93d
commit 5b2b2d8069
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Notation.lean
View file

@ -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