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

feat: reduce precedence of unary neg

Browse source
This commit is contained in:
Alex J. Best 2022-11-07 00:26:54 +01:00 • committed by Leonardo de Moura
parent 8da48f2381
commit 648ecff830
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/notation.md
View file

@ -7,7 +7,7 @@ overloading existing) prefix, infix, and postfix operators.
infixl:65 " + " => HAdd.hAdd -- left-associative
infix:50 " = " => Eq -- non-associative
infixr:80 " ^ " => HPow.hPow -- right-associative
prefix:100 "-" => Neg.neg
prefix:75 "-" => Neg.neg
# set_option quotPrecheck false
postfix:max "⁻¹" => Inv.inv
```
@ -26,7 +26,7 @@ can make this more precise by looking at what the commands above unfold to:
notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs
notation:80 lhs:81 " ^ " rhs:80 => HPow.hPow lhs rhs
notation:100 "-" arg:100 => Neg.neg arg
notation:75 "-" arg:75 => Neg.neg arg
# set_option quotPrecheck false
notation:1024 arg:1024 "⁻¹" => Inv.inv arg -- `max` is a shorthand for precedence 1024
```

2
src/Init/Notation.lean
View file

@ -263,7 +263,7 @@ syntax (name := rawNatLit) "nat_lit " num : term
@[inherit_doc] infixl:75 " >>> " => HShiftRight.hShiftRight
@[inherit_doc] infixr:80 " ^ " => HPow.hPow
@[inherit_doc] infixl:65 " ++ " => HAppend.hAppend
@[inherit_doc] prefix:100 "-" => Neg.neg
@[inherit_doc] prefix:75 "-" => Neg.neg
@[inherit_doc] prefix:100 "~~~" => Complement.complement
/-!