Skip to content

Commit

Permalink
doc: fix typo and make docstring more precise
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Nov 8, 2024
1 parent c779f3a commit 24f2edb
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Init/Notation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -71,9 +71,9 @@ def prio : Category := {}

/-- `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
Expand Down

0 comments on commit 24f2edb

Please sign in to comment.