michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(reserved_notation): make :: bind stronger than ++

Browse source 
this allows us to write l1 ++ a :: l2 without parentheses
This commit is contained in:
Floris van Doorn 2015-11-21 00:08:09 -05:00 committed by Leonardo de Moura
parent 5abc450fad
commit cc03ca9c6d
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/reserved_notation.hlean
View file

@ -152,4 +152,4 @@ reserve infix ` ⊇ `:50
reserve infix ` ∣ `:50
reserve infixl ` ++ `:65
reserve infixr ` :: `:65
reserve infixr ` :: `:67

2
library/init/reserved_notation.lean
View file

@ -193,7 +193,7 @@ reserve infix ` ⊇ `:50
reserve infix ` ∣ `:50
reserve infixl ` ++ `:65
reserve infixr ` :: `:65
reserve infixr ` :: `:67
infix + := add
infix * := mul