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

refactor(hott/init): 'prod' and 'sum' notation should be infix right like 'and' and 'or'

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-20 11:04:13 -08:00
parent 677ec2a2fe
commit 6843fe3a8b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/init/reserved_notation.hlean
View file

@ -46,8 +46,8 @@ reserve infixr `▸`:75
/- types and type constructors -/
reserve infixl `⊎`:25
reserve infixl `×`:30
reserve infixr `⊎`:25
reserve infixr `×`:30
/- arithmetic operations -/