diff --git a/BatteriesTest/help_cmd.lean b/BatteriesTest/help_cmd.lean index 23e3698b6d..f76f95c8c9 100644 --- a/BatteriesTest/help_cmd.lean +++ b/BatteriesTest/help_cmd.lean @@ -148,13 +148,12 @@ error: no syntax categories start with foobarbaz #help cats foobarbaz /-- -info: -category prec [Lean.Parser.Category.prec] +info: category prec [Lean.Parser.Category.prec] `prec` is a builtin syntax category for precedences. A precedence is a value that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is - parsed as `1 + (2 * 3)` because `*` has a higher pr0ecedence than `+`. + parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`. Higher numbers denote higher precedence. - In addition to literals like `37`, there are some special named priorities: + In addition to literals like `37`, there are some special named precedence levels: * `arg` for the precedence of function arguments * `max` for the highest precedence used in term parsers (not actually the maximum possible value) * `lead` for the precedence of terms not supposed to be used as arguments