Lean 语言参考手册

9. 属性🔗

属性是施加在声明上的一组可扩展编译期注解。 它们既可以作为声明修饰符添加，也可以用 Lean.Parser.Command.attribute : commandattribute 命令添加。

属性可以在编译期表中将信息与声明关联起来（包括自定义 simp 集、宏和实例），可以对定义施加额外要求（例如，当定义的类型不是类型类时拒绝它），也可以生成额外代码。 与项、命令和策略的宏及自定义精译器一样，属性的语法类别 attr 也被设计为可扩展的；有一张表将每个扩展映射到解释它的编译期程序。

属性以属性实例的形式应用；属性实例将一个作用域指示符与一个属性配成一对。 它们既可以出现在作为声明修饰符的属性中，也可以出现在独立的 Lean.Parser.Command.attribute : commandattribute 命令中。

语法属性实例
attrInstance ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind attr

attrKind 是可选的属性作用域关键字 local 或 scoped。 它们控制属性效果的可见范围。 属性本身可以是可扩展语法类别 attr 中的任何内容。

属性系统非常强大：属性可以将任意信息与声明关联起来，并生成任意数量的辅助声明。 这会带来一些设计上的取舍：存储这些信息会占用空间，检索它们则会耗费时间。 因此，有些属性只能应用于定义该声明的模块中的声明。 这样，在大型项目中查询会快得多，因为无需检查所有模块的数据。 每个属性自行决定如何存储其元数据，以及对特定用例而言，灵活性与性能之间怎样取舍才合适。

9.1. 作为修饰符的属性🔗

属性可以作为声明修饰符添加到声明上。 它们放在文档注释与可见性修饰符之间。

语法属性
attributes ::=
    @[attrInstance,*]

9.2. attribute 命令🔗

Lean.Parser.Command.attribute : commandattribute 命令可用于修改声明的属性。 一些用法示例包括：

  • 通过添加 instance，在局部作用域中将已有声明注册为实例；

  • 使用 simp 或 ext，将已有定理标记为 simp 引理或外延性引理；以及

  • 暂时从默认simp 集中移除一个 simp 引理。

语法修改属性

Lean.Parser.Command.attribute : commandattribute 命令为已有声明添加属性或从中移除属性。 标识符是要修改属性的名称。

command ::= ...
    | attribute [(eraseAttr | attrInstance),*] ident

除了用于向已有声明添加属性的属性实例之外，有些属性还可以被移除；这称为擦除属性。 在属性名称前加上 - 即可擦除该属性。 不过，并非所有属性都支持擦除。

语法擦除属性

在属性名称前加上 - 即可擦除该属性。

eraseAttr ::= ...
    | -ident

9.3. 有作用域的属性🔗

许多属性可以应用于特定作用域。 这决定了属性的效果是仅在当前小节作用域中可见、在打开当前命名空间的作用域内可见，还是处处可见。 这些作用域指示也用于控制语法扩展和类型类实例。 每个属性都负责精确定义这些术语对其特定效果意味着什么。

语法属性作用域

具有全局作用域的声明（默认情形）会在建立它们的模块被传递导入时生效。 不写其他作用域修饰符即表示全局作用域。

attrKind ::=
    `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。

具有局部作用域的声明只在建立它们的小节作用域范围内生效。

attrKind ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。local

具有命名空间作用域的声明会在建立它们的命名空间被打开时生效。

attrKind ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。scoped