翻译-Lean Language Reference-09-属性

属性 Attribute 是一组施加在声明上的可扩展的编译期注解。它们 可以作为声明修饰器添加，或者也 可以使用 attribute 命令添加。

属性可以 将信息与编译期表中的声明相关联（包括 自定义 simp 集、 宏和 类实例）、 对定义施加额外的要求（比方说如果它们的类型不是类类型就拒绝它们）以及 生成额外的代码。 属性的语法范畴 attr 与宏以及项、命令、策略的自定义阐释器一样也是可扩展的，并且 同样也存在着一张表可以将每个属性扩展映射到解释它的编译期程序。

属性会作为属性实例 Attribute Instance 被应用，它们将作用域指示器与属性配对。 这些实例要么 出现在声明修饰器中，要么 出现在独立的 attribute 命令中。

attrInstance ::= ...
  | attrKind attr

属性系统非常强大：属性可以 将任意信息与声明相关联，并且 生成任意数量的辅助函数。 这也带来了一些设计权衡： 存储这些信息需要空间，而 检索这些信息需要时间。因此， 某些属性只能应用于与声明所处相同模块中的声明。 如此便可提升大型项目中的查找效率， 因为它们不需要检查所有模块的数据。每个属性决定了 自己的元数据该如何存储，以及在特定的使用场景下 如何在灵活性和性能之间做出适当的权衡。

9.1. 属性作为修饰器 Attributes as Modifiers

属性可以作为声明修饰器被添加到声明上。它们应被置于文档注释和可见性修饰符之间。

attributes ::=
    @[attrInstance,*]

9.2. 属性命令 Attribute Commands

attribute 命令可用于修改声明的属性。一些示例用途包括：

• 将局部作用域中的已有声明注册为类实例 —— 这是通过添加 instance 实现的；

• 将已有定理标记为 simp 引理或外延性引理 —— 这是通过添加 simp 或 ext 实现的；

• 临时将一条 simp 引理从默认 simp 集合中移除。

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

除了可以通过属性实例向已有声明添加属性之外， 一部分属性也可以被移除。这种操作被称为属性擦除 Attribute Erasing。 属性可以通过在其名称前加上 - 来擦除。然而并非所有属性都支持擦除。

eraseAttr ::= ...
  | -ident

9.3. 带作用域的属性 Scoped Attributes

有不少属性可以被应用于特定的作用域中。这决定了属性的效果到底是 仅在当前节作用域中可见，还是 在打开当前命名空间的命名空间中可见，还是说 在任何地方都可见。 这些作用域指示器也被用于控制 语法扩展以及 类实例。 各个属性需要对这些项在特定的效果下到底意味着什么进行精确的定义。

attrKind ::=

attrKind ::= ...
  | local

attrKind ::= ...
  | scoped

索引 Index

术语

语法

常量

定理

公理

归纳

结构

类

选项

属性

例子