# 翻译-Lean Language Reference-09-属性

{{< ctxset prefix="9" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="术语" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="语法" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="常量" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="定理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="公理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="归纳" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="结构" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="类" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="选项" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

{{< labelindex 
  type="术语" 
  id_alias="属性"
  title_alias="属性 Attribute"
>}}
{{< /labelindex >}}**属性 Attribute** 是一组施加在声明上的可扩展的编译期注解。它们
可以作为[声明修饰器]({{< relref "read-LeanRef-web-Chpt07.md" >}}#术语-常量声明修饰器)添加，或者也
可以使用 `attribute` 命令添加。

属性可以
  将信息与编译期表中的声明相关联（包括
    [自定义 `simp` 集](https://lean-lang.org/doc/reference/latest/The-Simplifier/Simp-sets/#--tech-term-Custom-simp-sets)、
    [宏](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Macros/#--tech-term-Macros)和
    [类实例]({{< relref "read-LeanRef-web-Chpt10.md" >}}#术语-类实例)）、
  对定义施加额外的要求（比方说如果它们的类型不是类类型就拒绝它们）以及
  生成额外的代码。
属性的语法范畴 `attr` 与宏以及项、命令、策略的自定义阐释器一样也是可扩展的，并且
同样也存在着一张表可以将每个属性扩展映射到解释它的编译期程序。

属性会作为{{< labelindex 
  type="术语" 
  id_alias="属性实例"
  title_alias="属性实例 Attribute Instance"
>}}
{{< /labelindex >}}**属性实例 Attribute Instance** 被应用，它们将作用域指示器与属性配对。
这些实例要么
  出现在声明修饰器中，要么
  出现在独立的 `attribute` 命令中。

{{< labelindex 
  type="语法" 
  id_alias="属性实例"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
attrInstance ::= ...
  | attrKind attr
```

`attrKind` 为可选的[属性作用域](https://lean-lang.org/doc/reference/latest/Attributes/#scoped-attributes)关键字，可以是 `local` 或者是 `scoped`；
它们控制属性的可见性。属性本身可以是可扩展[语法范畴](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/#--tech-term-syntax-categories) `attr` 中的任何内容。
{{< /admonition >}}

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

## 9.1. 属性作为修饰器 Attributes as Modifiers {#S9-1}
{{< ctx level="2" >}}

属性可以作为[声明修饰器]({{< relref "read-LeanRef-web-Chpt07.md" >}}#术语-常量声明修饰器)被添加到声明上。它们应被置于文档注释和可见性修饰符之间。

{{< labelindex 
  type="语法" 
  id_alias="常量声明（属性实例补充）"
>}}
`@[…]`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
attributes ::=
    @[attrInstance,*]
```
{{< /admonition >}}

## 9.2. 属性命令 Attribute Commands {#S9-2}
{{< ctx level="2" >}}

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

- 将局部作用域中的已有声明注册为[类实例]({{< relref "read-LeanRef-web-Chpt10.md" >}}#术语-类实例) ——
  这是通过添加 `instance` 实现的；

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

- 临时将一条 `simp` 引理从默认 [`simp` 集合](https://lean-lang.org/doc/reference/latest/The-Simplifier/Simp-sets/#--tech-term-simp-set)中移除。

{{< labelindex 
  type="语法" 
  id_alias="常量属性修改"
>}}
`attribute […] …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
命令 `attribute` 用于向已有声明添加或移除属性。
标识符即对应属性正在被修改的名称。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | attribute [(eraseAttr | attrInstance),*] ident
```
{{< /admonition >}}

除了可以通过属性实例向已有声明添加属性之外，
一部分属性也可以被移除。这种操作被称为{{< labelindex 
  type="术语" 
  id_alias="属性擦除"
  title_alias="属性擦除 Attribute Erasing"
>}}
{{< /labelindex >}}**属性擦除 Attribute Erasing**。
属性可以通过在其名称前加上 `-` 来擦除。然而并非所有属性都支持擦除。

{{< labelindex 
  type="语法" 
  id_alias="常量属性擦除"
>}}
`-…`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
属性可通过在其名称前加上 `-` 来被擦除。

```lean {wrapper=false, lineNos=false}
eraseAttr ::= ...
  | -ident
```
{{< /admonition >}}

## 9.3. 带作用域的属性 Scoped Attributes {#S9-3}
{{< ctx level="2" >}}

有不少属性可以被应用于特定的作用域中。这决定了属性的效果到底是
  仅在当前节作用域中可见，还是
  在打开当前命名空间的命名空间中可见，还是说
  在任何地方都可见。
这些作用域指示器也被用于控制
  [语法扩展](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/#syntax-rules)以及
  [类实例]({{< relref "read-LeanRef-web-Chpt10.md" >}}#S10-2-5)。
各个属性需要对这些项在特定的效果下到底意味着什么进行精确的定义。

{{< labelindex 
  type="语法" 
  id_alias="常量受限属性实例补充"
>}}
`local`\
`scoped`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
具有全局作用域的声明（默认）
会在其所处的模块被传递导入时生效。
要表示它们只需省略其他作用域修饰符即可。

```lean {wrapper=false, lineNos=false}
attrKind ::=
```

具有局部作用域的声明
只会在它们所处的区段作用域中生效。

```lean {wrapper=false, lineNos=false}
attrKind ::= ...
  | local
```

具有受限作用域的声明
只会在它们所处的命名空间中生效。

```lean {wrapper=false, lineNos=false}
attrKind ::= ...
  | scoped
```
{{< /admonition >}}

## 索引 Index {#index}

### 术语

{{< indexlist type="术语" sort="title" >}}

### 语法

{{< indexlist type="语法" >}}

### 常量

{{< indexlist type="常量" code_wrap=true >}}

### 定理

{{< indexlist type="定理" code_wrap=true >}}

### 公理

{{< indexlist type="公理" code_wrap=true >}}

### 归纳

{{< indexlist type="归纳" code_wrap=true >}}

### 结构

{{< indexlist type="结构" code_wrap=true >}}

### 类

{{< indexlist type="类" code_wrap=true >}}

### 选项

{{< indexlist type="选项" code_wrap=true >}}

### 属性

{{< indexlist type="属性" code_wrap=true >}}

### 例子

{{< indexlist type="例子" print_section=false >}}

---

> 作者: [采石场的主人](https://ych817.github.io)  
> URL: https://ych817.github.io/posts/4c179c4/