文档注释 用于为其修饰的声明提供源码中的 API 文档。
需要注意，文档注释并不是真正意义上的“注释”：如果把文档注释放在不会被当作文档处理的位置，会产生语法错误。
在某些需要文本但转义会很繁琐的场景，文档注释也很有用，例如 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.
Basic example:
```lean
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is `(check all, whitespace := normalized, ordering := exact)`.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
(the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
Message ordering:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
This helps with testing commands that are non-deterministic in their ordering.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
#guard_msgs 命令中的期望消息。
docComment::=A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. /--...
-/
