command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      example `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig := term终止提示依次为 `termination_by` 和 `decreasing_by`。

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      example `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig
        (| term => term)*终止提示依次为 `termination_by` 和 `decreasing_by`。

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      example `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig where
        structInstField*