diff --git a/library/general_notation.lean b/library/general_notation.lean index b1ebfb0dd..ca7257d77 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -31,7 +31,7 @@ reserve infix `≈`:50 reserve infix `∼`:50 reserve postfix `⁻¹`:100 -reserve infixr `⬝`:75 +reserve infixl `⬝`:75 reserve infixr `▸`:75 -- ### types and type constructors diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean index 6b70b38a7..706ba0dcc 100644 --- a/tests/lean/interactive/eq2.lean +++ b/tests/lean/interactive/eq2.lean @@ -44,7 +44,7 @@ calc_trans eq.trans namespace eq_ops postfix `⁻¹` := eq.symm - infixr `⬝` := eq.trans + reserve infixr `⬝`:75 infixr `⬝` := eq.trans infixr `▸` := eq.subst end eq_ops open eq_ops