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

doc: fix max precedence

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-07 09:19:45 +02:00
parent 487bcaaf2b
commit 4517c518c8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/syntax.md
View file

@ -30,7 +30,7 @@ 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:1000 arg:1000 "⁻¹" => Inv.inv arg -- `max` is a shorthand for precedence 1000
notation:1024 arg:1024 "⁻¹" => Inv.inv arg -- `max` is a shorthand for precedence 1024
```
It turns out that all commands from the first code block are in fact command *macros* translating to the more general `notation` command.