4.4. 归纳类型🔗

感应类型是向Lean引入新类型的主要手段。虽然 universes、functions 和 quotient types 是用户无法添加的内置原语，但 Lean 中的所有其他类型要么是归纳类型，要么是根据 Universe、函数和归纳类型定义的。归纳类型由其 type 构造函数 及其 constructors 指定；它们的其他属性都是从这些派生的。每个归纳类型都有一个类型构造函数，它可以同时采用全域参数和普通参数。归纳类型可以有任意数量的构造函数；这些构造函数引入了新值，其类型以归纳类型的类型构造函数为首。

基于类型构造函数和归纳类型的构造函数，Lean 派生 recursor。逻辑上，递归代表归纳原则或消除规则；在计算上，它们代表原始的递归计算。递归函数的终止是通过将它们转换为递归器的使用来证明的，因此 Lean 的内核只需要执行递归应用程序的类型检查，而不需要包括单独的终止分析。 Lean 另外还生成许多基于递归器的辅助构造，始终使用术语recursor，即使对于非递归类型也是如此。它们在系统的其他地方使用。

结构是归纳类型的一种特殊情况，只有一个构造函数。声明结构时，Lean 会生成帮助程序，使其他语言功能能够与新结构一起使用。

本节介绍用于指定归纳类型和结构的语法的具体细节、环境中由归纳类型声明产生的新常量和定义，以及编译代码中归纳类型' 值的运行时表示。

4.4.1. 归纳类型声明🔗

syntaxInductive Type Declarations

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

声明新的归纳类型。 declModifiers 的含义如关于声明修饰符部分所述。

声明归纳类型后，其类型构造函数、构造函数和递归器将出现在环境中。新的归纳类型扩展了 Lean 的核心逻辑 - 它们不由其他一些已存在的数据编码或表示。归纳类型声明必须满足许多格式良好的要求，以确保逻辑保持一致。

声明的第一行，从 Lean.Parser.Command.inductive : commandinductive 到 Lean.Parser.Command.inductive : commandwhere，指定新的类型构造函数的名称和类型。如果提供了类型构造函数的类型签名，则其结果类型必须是 universe，但参数不需要是类型。如果未提供签名，则 Lean 将尝试推断一个刚好足以包含结果类型的 Universe。在某些情况下，此过程可能无法找到最小宇宙或根本找不到最小宇宙，因此需要注释。

构造器规范遵循Lean.Parser.Command.inductive : commandwhere。构造函数不是强制性的，因为无构造函数的归纳类型（例如 False 和 Empty）是完全合理的。每个构造函数规范均以竖线（'|'、Unicode 'VERTICAL BAR' (U+007c)）、声明修饰符和名称开头。该名称是原始标识符。名称后面有声明签名。签名可以指定任何参数，以归纳类型声明的格式良好性要求为模，但签名中的返回类型必须是指定的归纳类型的类型构造函数的饱和应用程序。如果未提供签名，则通过插入足够的隐式参数来构造格式正确的返回类型来推断构造函数的类型。

新归纳类型的名称在当前命名空间中定义。每个构造函数的名称位于归纳类型的命名空间中。

4.4.1.1. 参数及指标🔗

Type 构造函数可以采用两种参数： parameters 和 indices. 整个定义中参数的使用必须一致；声明中每个构造函数中所有出现的类型构造函数都必须采用完全相同的参数。索引可能因类型构造函数的出现而异。所有参数必须位于类型构造函数签名中的所有索引之前。

类型构造函数签名中冒号 (':') 之前出现的参数被视为整个归纳类型声明的参数。它们始终是在整个类型定义中必须保持一致的参数。一般来说，出现在冒号之后的参数是在整个类型定义中可能变化的索引。然而，如果选项 inductive.autoPromoteIndices 是 true，则本来可以是参数的语法索引将变成参数。如果索引的所有类型依赖项本身都是参数，并且在所有构造函数中出现的归纳类型类型构造函数中统一用作未实例化的变量，则索引可能是参数。

option

inductive.autoPromoteIndices

Default value: true

Promote indices to parameters in inductive types whenever possible.

索引可以被视为定义类型的family。每个索引选择都会从该族中选择一个类型，该族有自己的一组可用构造函数。据说带有索引的 Type 构造函数指定类型的 indexed family 。

4.4.1.2. 示例归纳类型🔗

A constructorless type

Vacant 是一个空的归纳类型，相当于 Lean 的 Empty 类型：

inductive Vacant : Type where

空的归纳类型并不是没有用；它们可用于指示无法访问的代码。

Live ↪

A constructorless proposition

No 是一个假命题，等价于 Lean 的 False：

inductive No : Prop where

Live ↪

A unit type

Solo 相当于 Lean 的 Unit 类型：

inductive Solo where
  | solo

这是归纳类型的示例，其中类型构造函数和构造函数的签名均被省略。 Lean 将 Solo 分配给 Type：

Solo : Type#check Solo

Solo : Type

该构造函数被命名为 Solo.solo，因为构造函数名称是类型构造函数的命名空间。由于 Solo 不需要任何参数，因此为 Solo.solo 推断的签名为：

Solo.solo : Solo#check Solo.solo

Solo.solo : Solo

Live ↪

A true proposition

Yes 等价于 Lean 的 True 命题：

inductive Yes : Prop where
  | intro

与 One 不同，新的归纳类型Yes 被指定位于 Prop Universe 中。

Yes : Prop#check Yes

Yes : Prop

Yes.intro 推断的签名是：

Yes.intro : Yes#check Yes.intro

Yes.intro : Yes

Live ↪

A type with parameter and index

EvenOddList α b 是一个列表，其中 α 是列表中存储的数据类型，当条目数为偶数时，b 是 true：

inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

此示例的类型正确，因为列表中有两个条目：

example : EvenOddList String true :=
  .cons "a" (.cons "b" .nil)

此示例的类型不正确，因为列表中有三个条目：

example : EvenOddList String true :=
  Type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true
but is expected to have type
  EvenOddList String true.cons "a" (.cons "b" (.cons "c" .nil))

Type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true
but is expected to have type
  EvenOddList String true

在此声明中，α 是参数，因为它在所有出现的 EvenOddList 中一致使用。 b 是索引，因为它在不同的情况下使用不同的 Bool 值。

Live ↪

Parameters before and after the colon

在此示例中，两个参数均在 Either 签名中的冒号之前指定。

inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | left : α → Either α β
  | right : β → Either α β

在此版本中，有两种名为 α 的类型可能不相同：

inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
  Mismatched inductive type parameter in
  Either' α β
The provided argument
  α
is not definitionally equal to the expected parameter
  α✝

Note: The value of parameter `α✝` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.| left : {α : Type u} → {β : Type v} → α → Either' α β
  | right : β → Either' α β

Mismatched inductive type parameter in
  Either' α β
The provided argument
  α
is not definitionally equal to the expected parameter
  α✝

Note: The value of parameter `α✝` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.

将参数放在冒号后面会产生可由构造函数实例化的参数：

inductive Either'' : Type u → Type v → Type (max u v + 1) where
  | left : {α : Type u} → {β : Type v} → α → Either'' α β
  | right : β → Either'' α β

此类型需要更大的 Universe，因为构造函数参数必须位于比归纳类型的 Universe 小的 Universe 中。 Either''.right 的类型参数是通过 Lean 的自动隐式参数的普通规则发现的。

Live ↪

4.4.1.3. 匿名构造函数语法🔗

如果归纳类型只有一个构造函数，则该构造函数符合 匿名构造函数语法。可以将显式参数括在尖括号（'⟨' 和 '⟩'、Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) 和 MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)）中并用逗号分隔，而不是将构造函数的名称写入其参数。这在模式和表达式上下文中都有效。按名称提供参数或使用 @ 将所有隐式参数转换为显式参数需要使用普通构造函数语法。

syntaxAnonymous Constructors

可以通过将构造函数的显式参数括在尖括号中并用逗号分隔来匿名调用。

term ::= ...
    | The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
expected type is an inductive type with a single constructor `c`.
If more terms are given than `c` has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
⟨ term,* ⟩

Anonymous constructors

AtLeastOne α 类型与 List α 类似，只不过始终至少存在一个元素：

inductive AtLeastOne (α : Type u) : Type u where
  | mk : α → Option (AtLeastOne α) → AtLeastOne α

可以使用匿名构造函数语法来构造它们：

def oneTwoThree : AtLeastOne Nat :=
  ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩

并与他们匹配：

def AtLeastOne.head : AtLeastOne α → α
  | ⟨x, _⟩ => x

同样，可以使用传统的构造函数语法：

def oneTwoThree' : AtLeastOne Nat :=
  .mk 1 (some (.mk 2 (some (.mk 3 none))))

def AtLeastOne.head' : AtLeastOne α → α
  | .mk x _ => x

Live ↪

4.4.1.4. 派生实例🔗

归纳类型声明的可选 Lean.Parser.Command.inductive : commandderiving 子句可用于派生类型类的实例。更多信息请参考实例派生部分。

4.4.2. 结构声明🔗

syntaxStructure Declarations

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      structure `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` bracketedBinder* (: term)?
        (extends (ident : )?term,*)?
        where
        (`declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident ::)?
        structFields
      (deriving derivingClass,*)?

声明一个新的结构类型。

结构是仅具有单个构造函数且没有索引的归纳类型。作为这些限制的交换，Lean 为结构生成代码，提供了许多便利：为每个字段生成投影函数，可以使用基于字段名称而不是位置参数的附加构造函数语法，可以使用类似的语法来替换某些命名字段的值，并且结构可以扩展其他结构。就像其他归纳类型一样，结构可以是递归的；他们在严格积极性方面受到同样的限制。结构不会给Lean增加任何表现力；它们的所有功能都是通过代码生成来实现的。

4.4.2.1. 结构参数🔗

就像普通的归纳类型声明一样，结构声明的标头包含一个可以指定参数和结果 Universe 的签名。结构不能定义索引族。

4.4.2.2. 领域🔗

结构声明的每个字段对应于构造函数的一个参数。

Inferring Universes

MyProd 的结构与 Prod 相同。

structure MyProd (α β : Type _) where
  fst : α
  snd : β

这两个参数和两个字段是构造函数参数：

MyProd.mk.{u, v}
  {α : Type u}
  {β : Type v}
  (fst : α)
  (snd : β)
  : MyProd.{u, v} α β

另外，构造函数为universe polymorphic；类型构造函数 MyProd 采用两个 Universe 参数：

MyProd.{u, v} (α : Type u) (β : Type v) : Type (max u v)

每个字段的每种类型的宇宙层级必须小于或等于结构体的宇宙层级。 Lean 推断 Type (max u v) 是可以容纳 Type u 和 Type v 的最小宇宙。

Live ↪

自动隐式参数会单独插入到每个字段中，即使它们的名称相同，并且这些字段会成为对类型进行量化的构造函数参数。

Auto-Implicit Parameters in Structure Fields

结构 MyStructure 包含其类型具有自动隐式参数的字段：

structure MyStructure where
  field1 : Fin n
  field2 : Fin n

构造函数 MyStructure.mk 中的每个字段都有自己的隐式参数 n，其类型为 Nat：

MyStructure.mk
  (field1 : {n : Nat} → Fin n)
  (field2 : {n : Nat} → Fin n)
  : MyStructure

类型构造函数 MyStructure 不采用 Universe 参数，结果类型位于 Type 中，这是 Nat 和 Fin n 的宇宙：

MyStructure : Type

Live ↪

对于每个字段，都会生成一个投影函数，用于从基础类型的构造函数中提取字段的值。该函数位于结构名称的命名空间中。结构字段投影由精化器专门处理（如有关结构继承的部分中所述），它执行查找命名空间之外的额外步骤。当字段类型依赖于先前字段时，依赖投影函数的类型根据早期投影来编写，而不是显式的模式匹配。

Dependent projection types

结构体 ArraySized 包含一个字段，其类型取决于结构体参数和之前的字段：

structure ArraySized (α : Type u) (length : Nat)  where
  array : Array α
  size_eq_length : array.size = length

投影函数 size_eq_length 的签名将结构类型的参数作为隐式参数，并使用相应的投影引用先前的字段：

ArraySized.size_eq_length.{u}
  {α : Type u} {length : Nat}
  (self : ArraySized α length)
  : self.array.size = length

Live ↪

结构字段可能有默认值，用 := 指定。如果未提供明确的值，则使用这些值。

Default values

图的邻接列表表示可以表示为 Nat 列表的数组。数组的大小表示顶点的数量，每个顶点的出边都存储在数组中顶点的索引处。由于为字段 adjacency 提供了默认值 #[]，因此可以在不提供任何字段值的情况下构造空图 Graph.empty。

structure Graph where
  adjacency : Array (List Nat) := #[]

def Graph.empty : Graph := {}

Live ↪

结构字段还可以使用点表示法通过其索引进行访问。字段编号以 1 开头。

4.4.2.3. 结构构造函数🔗

可以通过在字段之前提供构造函数名称和 :: 来显式命名结构构造函数。如果未显式提供名称，则构造函数在结构类型的命名空间中命名为 mk。声明修饰符还可以与显式构造函数名称一起提供。

Non-default constructor name

结构体 Palindrome 包含一个字符串和一个字符串反转后相同的证明：

structure Palindrome where
  ofString ::
  text : String
  is_palindrome : text.`String.data` has been deprecated: Use `String.toList` insteaddata.reverse = text.`String.data` has been deprecated: Use `String.toList` insteaddata

其构造函数名为 Palindrome.ofString，而不是 Palindrome.mk。

Live ↪

Modifiers on structure constructor

结构 NatStringBimap 保持自然数和字符串之间的有限双射。它由一对映射组成，每个键都作为值在另一个映射中仅出现一次。由于构造函数是私有的，因此定义模块外部的代码无法构造新实例，并且必须使用提供的 API，它维护类型的不变量。此外，显式提供默认构造函数名称可以将文档注释附加到构造函数。

structure NatStringBimap where
  /--
  Build a finite bijection between some
  natural numbers and strings
  -/
  private mk ::
  natToString : Std.HashMap Nat String
  stringToNat : Std.HashMap String Nat

def NatStringBimap.empty : NatStringBimap := ⟨{}, {}⟩

def NatStringBimap.insert
    (nat : Nat) (string : String)
    (map : NatStringBimap) :
    Option NatStringBimap :=
  if map.natToString.contains nat ||
      map.stringToNat.contains string then
    none
  else
    some <|
      NatStringBimap.mk
        (map.natToString.insert nat string)
        (map.stringToNat.insert string nat)

Live ↪

由于结构由单构造函数归纳类型表示，因此可以使用匿名构造函数语法调用或匹配其构造函数。此外，可以使用 结构实例表示法来构造或匹配结构，其中包括字段的名称及其值。

syntaxStructure Instances

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{ structInstField,*
        (: term)? }

构造一个构造函数类型的值，给定命名字段的值。字段说明符可以采用两种形式：

structInstField ::= ...
    | structInstLVal := private? term

structInstField ::= ...
    | ident

structInstLVal 是字段名称（标识符）、字段索引（自然数）或方括号中的术语，后跟零个或多个子字段的序列。子字段可以是前面带有点的字段名称或索引，也可以是方括号中的术语。

该语法针对结构构造函数的应用进行了详细精化。为字段提供的值是按名称提供的，并且可以按任何顺序提供。为子字段提供的值用于初始化结构构造函数的字段，这些结构本身在字段中找到。构造结构时不允许使用方括号中的术语；它们用于结构更新。

不包含 := 的字段说明符是字段缩写。在本文中，标识符f是f := f的缩写；即用当前作用域中f的值来初始化字段f。

必须提供每个没有默认值的字段。如果将策略指定为默认参数，则它将在精化时间运行以构造参数的值。

在模式上下文中，字段名称映射到与相应投影匹配的模式，并且字段缩写绑定作为字段名称的模式变量。默认参数仍然存在于模式中；如果模式没有为具有默认值的字段指定值，则该模式仅与默认值匹配。

当字段定义包含 Lean.Parser.Term.stuctInstFieldprivate 修饰符时，该值将放置在当前模块的私有范围中，即使结构值本身位于公共范围中也是如此。该值包含在公共但未公开的帮助器定义中。这对于类型类的实例特别有用，因为默认情况下，类型类的公共实例中方法的实现是暴露。此修饰符允许将它们设为私有。

可选的类型注释允许在未另行确定的上下文中指定结构类型。

Patterns and default values

结构 AugmentedIntList 包含一个列表以及一些额外信息，如果省略则为空：

structure AugmentedIntList where
  list : List Int
  augmentation : String := ""

当测试列表是否为空时，函数 isEmpty 必须显式匹配 augmentation 字段，即使它有默认值：

def AugmentedIntList.isEmpty : AugmentedIntList → Bool
  | {list := [], augmentation := ""} => true
  | _ => false

false#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty

false

Live ↪

Private Field Values

即使结构的定义为 exposeed，也可以使用字段级 Lean.Parser.Term.stuctInstFieldprivate 修饰符隐藏各个字段。在此模块中，x 的公开公共定义可以使用私有定义 secret，因为 imaginary 字段的值未公开：

Main.lean

module

public structure Complex where
  real : Float
  imaginary : Float

private def secret := 2.3

@[expose]
public def x : Complex := {
  real := 5.0
  imaginary := private 2 * secret
}

Private Methods

在此模块中，State 结构的存在是公共的，但其构造函数和字段是私有的。函数 State.toString 也是私有的，旨在通过 ToString 实例进行访问。但是，由于 methods 的实现是针对公共实例公开的，因此不允许这样做：

Main.lean

module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := s.Invalid field `toString`: The environment does not contain `State.toString`, so it is not possible to project the field `toString` from an expression
  s
of type `State`

Note: A private declaration `State.toString` (from the current module) exists but would need to be public to access here.toString

Invalid field `toString`: The environment does not contain `State.toString`, so it is not possible to project the field `toString` from an expression
  s
of type `State`

Note: A private declaration `State.toString` (from the current module) exists but would need to be public to access here.

将 toString 的实现标记为 private 会将其从模块的公共范围中删除，从而使其能够访问私有函数：

Main.lean

module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := private s.toString

syntaxStructure Updates

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{term with
        structInstField,*
        (: term)?}

更新构造函数类型的值。 Lean.Parser.Term.structInst : termStructure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be inherited. If `e` is itself a variable called `x`, it can be elided: `fun y => { x := 1, y }`. A *structure update* of an existing value can be given via `with`: `{ point with x := 1 }`. The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`.with 子句之前的术语应具有结构类型；这是正在更新的值。创建结构的新实例，其中未指定的每个字段都是从正在更新的值复制的，并且指定的字段将替换为其新值。更新结构时，还可以通过将要更新的索引包含在方括号中来替换数组值。此更新不要求索引表达式位于数组的范围内，并且超出范围的更新将被丢弃。

Updating arrays

更新结构可以使用数组索引以及投影名称。超出范围的索引更新将被忽略：

structure AugmentedIntArray where
  array : Array Int
  augmentation : String := ""
deriving Repr

def one : AugmentedIntArray := {array := #[1]}
def two : AugmentedIntArray := {one with array := #[1, 2]}
def two' : AugmentedIntArray := {two with array[0] := 2}
def two'' : AugmentedIntArray := {two with array[99] := 3}
({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })#eval (one, two, two', two'')

({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })

结构类型的值也可以使用 Lean.Parser.Command.declValEqns : commandwhere 声明，后跟每个字段的定义。这只能用作定义的一部分，不能在表达式上下文中使用。

where for structures

Lean 中的产品类型是名为 Prod 的结构。产品可以使用它们的投影来定义：

def location : Float × Float where
  fst := 22.807
  snd := -13.923

4.4.2.4. 结构继承🔗

可以使用可选的 Lean.Parser.Command.structure : commandextends 子句将结构声明为扩展其他结构。生成的结构类型具有所有父结构类型的所有字段。如果父结构类型具有重叠的字段名称，则所有重叠的字段名称必须具有相同的类型。

生成的结构具有影响字段值的 字段解析顺序。如果可能，此解析顺序是结构父级的 C3 线性化。本质上，字段解析顺序应该是整个父集的总排序，以便每个 Lean.Parser.Command.structure : commandextends 列表都是有序的。当没有 C3 线性化时，仍然会使用启发式来查找阶数。每个结构类型都按照其自己的字段解析顺序排列在第一位。

字段解析顺序用于计算可选字段的默认值。当未指定字段值时，将使用解析顺序中定义的第一个默认值。对默认值中字段的引用也使用字段解析顺序；这意味着覆盖父构造函数默认字段的子结构也可能会更改父字段的计算默认值。由于子结构是其自身解析顺序的第一个元素，因此子结构中的默认值优先于父结构中的默认值。

当新结构扩展现有结构时，新结构的构造函数将现有结构的信息作为附加参数。通常，这采用每个父结构类型的构造函数参数的形式。该父值包含父级的所有字段。然而，如果父级的字段重叠，则包括来自一个或多个父级的非重叠字段的子集，而不是父级结构的整个值，以防止重复字段信息。

父结构类型与其子结构类型之间不存在子类型关系。即使结构体 B 扩展结构体 A，需要 A 的函数也不会接受 B。但是，会生成将结构转换为其每个父结构的转换函数。这些转换函数称为 parentprojections。父投影位于子结构的命名空间中，其名称是父结构的名称，前面带有 to。

Structure type inheritance with overlapping fields

在此示例中，Textbook 是 Book，同时也是 AcademicWork：

structure Book where
  title : String
  author : String

structure AcademicWork where
  author : String
  discipline : String

structure Textbook extends Book, AcademicWork

Textbook.toBook (self : Textbook) : Book#check Textbook.toBook

由于字段 author 出现在 Book 和 AcademicWork 中，因此构造函数 Textbook.mk 不会将两个父项都作为参数。它的签名是：

Textbook.mk (toBook : Book) (discipline : String) : Textbook

转换函数为：

Textbook.toBook (self : Textbook) : BookTextbook.toAcademicWork (self : Textbook) : AcademicWork

后者将包含的 Book 的 author 字段与非捆绑的 Discipline 字段组合在一起，相当于：

def toAcademicWork (self : Textbook) : AcademicWork :=
  let .mk book discipline := self
  let .mk _title author := book
  .mk author discipline

Live ↪

可以使用生成的结构的投影，就好像它的字段只是父字段的并集一样。当使用字段时，Lean精化器自动生成适当的投影。同样，基于字段的初始化和结构更新符号隐藏了继承编码的细节。但是，当使用构造函数的名称、使用匿名构造函数语法或通过索引而不是名称引用字段时，编码是可见的。

Field Indices and Structure Inheritance

structure Pair (α : Type u) where
  fst : α
  snd : α
deriving Repr

structure Triple (α : Type u) extends Pair α where
  thd : α
deriving Repr

def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}

计算 coords 的第一个字段索引会生成基础 Pair，而不是字段 fst 的内容：

{ fst := 17, snd := 2 }#eval coords.1

{ fst := 17, snd := 2 }

精化器将 coords.fst 转换为 coords.toPair.fst。

Live ↪

No structure subtyping

给出偶数、偶素数和具体偶素数的定义：

structure EvenNumber where
  val : Nat
  isEven : 2 ∣ val := by decide

structure EvenPrime extends EvenNumber where
  notOne : val ≠ 1 := by decide
  isPrime : ∀ n, n ≤ val → n ∣ val  → n = 1 ∨ n = val

def two : EvenPrime where
  val := 2
  isPrime := by⊢ ∀ (n : Nat), n ≤ 2 → n ∣ 2 → n = 1 ∨ n = 2
    introsn✝:Nata✝¹:n✝ ≤ 2a✝:n✝ ∣ 2⊢ n✝ = 1 ∨ n✝ = 2
    repeat' (cases ‹Nat.le _ _›step.step.refl.refla✝:0 ∣ 2⊢ 0 = 1 ∨ 0 = 2)
    all_goals omegaAll goals completed! 🐙

def printEven (num : EvenNumber) : IO Unit :=
  IO.print num.val

将 printEven 直接应用于 two 是类型错误：

printEven sorry : IO Unit#check printEven Application type mismatch: The argument
  two
has type
  EvenPrime
but is expected to have type
  EvenNumber
in the application
  printEven twotwo

Application type mismatch: The argument
  two
has type
  EvenPrime
but is expected to have type
  EvenNumber
in the application
  printEven two

因为 EvenPrime 类型的值并不是 EvenNumber 类型的值。

Lean.Parser.Command.print : command#print 命令显示有关结构类型的最重要信息，包括父投影、所有字段及其默认值、构造函数和字段解析顺序。当处理包含继承菱形的深层层次结构时，此信息可能非常有用。

#print and Structure Types

该结构类型集合模拟了各种自行车，包括电动自行车和非电动自行车，以及普通尺寸和大型家庭自行车。最终结构类型 ElectricFamilyBike 在其继承图中包含菱形，因为 FamilyBike 和 ElectricBike 都扩展了 Bicycle。

structure Vehicle where
  wheels : Nat

structure Bicycle extends Vehicle where
  wheels := 2

structure ElectricVehicle extends Vehicle where
  batteries : Nat := 1

structure FamilyBike extends Bicycle where
  wheels := 3

structure ElectricBike extends Bicycle, ElectricVehicle

structure ElectricFamilyBike
    extends FamilyBike, ElectricBike where
  batteries := 2

Lean.Parser.Command.print : command#print 命令显示有关每种结构类型的重要信息：

structure ElectricBike : Type
number of parameters: 0
parents:
  ElectricBike.toBicycle : Bicycle
  ElectricBike.toElectricVehicle : ElectricVehicle
fields:
  Vehicle.wheels : Nat :=
    2
  ElectricVehicle.batteries : Nat :=
    1
constructor:
  ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
field notation resolution order:
  ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricBike

structure ElectricBike : Type
number of parameters: 0
parents:
  ElectricBike.toBicycle : Bicycle
  ElectricBike.toElectricVehicle : ElectricVehicle
fields:
  Vehicle.wheels : Nat :=
    2
  ElectricVehicle.batteries : Nat :=
    1
constructor:
  ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
field notation resolution order:
  ElectricBike, Bicycle, ElectricVehicle, Vehicle

ElectricFamilyBike 默认情况下具有三个轮子，因为 FamilyBike 的分辨率顺序先于 Bicycle：

structure ElectricFamilyBike : Type
number of parameters: 0
parents:
  ElectricFamilyBike.toFamilyBike : FamilyBike
  ElectricFamilyBike.toElectricBike : ElectricBike
fields:
  Vehicle.wheels : Nat :=
    3
  ElectricVehicle.batteries : Nat :=
    2
constructor:
  ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
field notation resolution order:
  ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricFamilyBike

structure ElectricFamilyBike : Type
number of parameters: 0
parents:
  ElectricFamilyBike.toFamilyBike : FamilyBike
  ElectricFamilyBike.toElectricBike : ElectricBike
fields:
  Vehicle.wheels : Nat :=
    3
  ElectricVehicle.batteries : Nat :=
    2
constructor:
  ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
field notation resolution order:
  ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle

Live ↪

4.4.3. 逻辑模型🔗

4.4.3.1. 递归器🔗

每个归纳类型都配备有 recursor。递归器完全由类型构造函数和构造函数的签名确定。递归器具有函数类型，但它们是原始类型，无法使用 fun 进行定义。

4.4.3.1.1. 递归器类型🔗

递归器采用以下参数：

归纳类型的参数: 由于参数是一致的，因此可以在整个递归器上抽象它们。
motive: 动机决定了递归器的应用类型。动机是一个函数，其参数是类型的索引和实例化这些索引的类型的实例。动机确定的类型的特定 Universe 取决于归纳类型的 Universe 和特定构造函数 - 有关详细信息，请参阅有关 subsingleton 消除的部分。
每个构造函数都有一个 小前提: 对于每个构造函数，递归器期望一个函数满足构造函数的任意应用的动机。每个小前提都抽象了构造函数的所有参数。如果构造函数的参数类型是归纳类型本身，则小前提另外接受一个参数，该参数的类型是应用于该参数值的动机 - 这将收到递归处理递归参数的结果。
大前提，或目标: 最后，递归器将类型的实例以及任何索引值作为参数。

递归器的结果类型是应用于这些索引的动机和大前提。

The recursor for Bool

Bool的递归器Bool.rec具有以下参数：

动机计算任何宇宙中的类型，给定 Bool。
两个构造函数都有一些小前提，其中 false 和 true 的动机都得到满足。
大前提是一些Bool。

返回类型是应用于大前提的动机。

Bool.rec.{u} {motive : Bool → Sort u}
  (false : motive false)
  (true : motive true)
  (t : Bool) : motive t

The recursor for List

List的递归器List.rec具有以下参数：

参数α排在第一位，因为动机、小前提、大前提都需要引用它。
动机计算任何宇宙中的类型，给定 List α。宇宙层级 u 和 v 之间没有连接。
两个构造函数都有一些小前提：
- List.nil 的动机得到满足
- 动机应该可以满足 List.cons 的任何应用，因为它可以满足尾部。额外的参数motive tail是因为tail的类型是List的递归出现。
大前提是一些List α。

再次强调，返回类型是应用于大前提的动机。

List.rec.{u, v} {α : Type v} {motive : List α → Sort u}
  (nil : motive [])
  (cons : (head : α) → (tail : List α) → motive tail →
    motive (head :: tail))
  (t : List α) : motive t

Recursor with parameters and indices

给出 EvenOddList 的定义：

inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

递归器 EvenOddList.rec 与 List 非常相似。差异来自于索引的存在：

现在的动机抽象了任何任意选择的指数。
nil 的小前提将动机应用于 nil 的索引值 true。
小前提cons对其递归发生中使用的索引值进行抽象，并用其否定实例化动机。
大前提还抽象了任意选择的索引。

EvenOddList.rec.{u, v} {α : Type v}
  {motive : (isEven : Bool) → EvenOddList α isEven → Sort u}
  (nil : motive true EvenOddList.nil)
  (cons : {isEven : Bool} →
    (head : α) →
    (tail : EvenOddList α isEven) → motive isEven tail →
    motive (!isEven) (EvenOddList.cons head tail)) :
  {isEven : Bool} → (t : EvenOddList α isEven) → motive isEven t

Live ↪

当使用谓词（即返回 Prop 的函数）作为动机时，递归表示归纳。非递归构造函数的小前提是基例，为具有递归参数的构造函数的小前提提供的附加参数是归纳假设。

4.4.3.1.1.1. 亚单例消除🔗

Lean 中的证明与计算无关。换句话说，在提供了某个命题的“某些”证明后，程序应该不可能检查它收到了“哪个”证明。这反映在归纳定义的命题或谓词的递归器类型中。对于这些类型，如果该定理有多个潜在证明，则动机可能只会返回另一个 Prop。如果类型的结构使得最多只有一个证明，那么动机可能会返回任何宇宙中的类型。最多有一个居民的命题称为 subsingleton。不是强迫用户证明只有一种可能的证明，而是使用保守的语法近似来检查命题是否是子单例。满足以下两个要求的提案被视为子单例：

最多有一个构造函数。
每个构造函数的参数类型都是 Prop、参数或索引。

True is a subsingleton

True 是一个子单例，因为它有一个构造函数，并且该构造函数没有参数。其递归器具有以下签名：

True.rec.{u} {motive : True → Sort u}
  (intro : motive True.intro)
  (t : True) : motive t

False is a subsingleton

False 是一个子单例，因为它没有构造函数。其递归器具有以下签名：

False.rec.{u} (motive : False → Sort u) (t : False) : motive t

请注意，动机是一个显式参数。这是因为在任何进一步的参数类型中都没有提到它，因此无法通过统一来解决。

And is a subsingleton

And 是一个子单例，因为它有一个构造函数，并且构造函数的两个参数类型都是命题。其递归器具有以下签名：

And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u}
  (intro : (left : a) → (right : b) → motive (And.intro left right))
  (t : a ∧ b) : motive t

Or is not a subsingleton

Or 不是子单例，因为它有多个构造函数。其递归器具有以下签名：

Or.rec {a b : Prop} {motive : a ∨ b → Prop}
  (inl : ∀ (h : a), motive (.inl h))
  (inr : ∀ (h : b), motive (.inr h))
  (t : a ∨ b) : motive t

动机的类型表明Or.rec只能用于产生证明。析取的证明可以用来证明其他东西，但是程序无法检查两个析取中哪一个为真并用于证明。

Eq is a subsingleton

Eq 是一个子单例，因为它只有一个构造函数 Eq.refl。此构造函数使用参数值实例化 Eq 的索引，因此所有参数都是参数：

Eq.refl.{u} {α : Sort u} (x : α) : Eq x x

其递归器具有以下签名：

Eq.rec.{u, v} {α : Sort v} {x : α}
  {motive : (y : α) → x = y → Sort u}
  (refl : motive x (.refl x))
  {y : α} (t : x = y) : motive y t

这意味着等式证明可以用来重写非命题的类型。

4.4.3.1.2. 减少🔗

除了向逻辑添加新常量之外，归纳类型声明还添加新的归约规则。这些规则控制着递归器和构造函数之间的交互；特别是以构造函数作为主要前提的递归器。这种形式的还原称为 ι-还原（iota 还原）。

当递归器的大前提是不带递归参数的构造函数时，递归应用程序会简化为构造函数的小前提对构造函数的参数的应用。如果存在递归参数，则通过将递归应用于递归事件来找到小前提的这些参数。

4.4.3.2. 格式良好的要求🔗

归纳类型声明须遵守许多格式良好的要求。这些要求确保 Lean 在使用归纳类型的新规则进行扩展时保持逻辑一致。他们是保守的：存在潜在的归纳类型不会破坏一致性，但这些要求仍然拒绝。

4.4.3.2.1. 宇宙层级🔗

归纳类型的 Type 构造函数必须位于 universe 或其返回类型为 Universe 的函数类型中。每个构造函数必须位于返回归纳类型的饱和应用程序的函数类型中。如果归纳类型的 Universe 是 Prop，则对 Universe 没有进一步的限制，因为 Prop 是必然。如果 Universe 不是 Prop，则构造函数的每个参数必须满足以下条件：

如果构造函数的参数是归纳类型的参数（在参数与索引的意义上），则此参数的类型可能不大于类型构造函数的范围。
所有其他构造函数参数必须小于类型构造函数的范围。

Universes, constructors, and parameters

Either 位于其参数的较大宇宙中，因为两者都是归纳类型的参数：

inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | inl : α → Either α β
  | inr : β → Either α β

CanRepr 位于比构造函数参数 α 更大的宇宙中，因为 α 不是归纳类型的参数之一：

inductive CanRepr : Type (u + 1) where
  | mk : (α : Type u) → [Repr α] → CanRepr

无构造函数归纳类型可能位于比其参数更小的宇宙中：

inductive Spurious (α : Type 5) : Type 0 where

但是，在不更改其级别的情况下向 Spurious 添加构造函数是不可能的。

Live ↪

4.4.3.2.2. 严格的积极性🔗

在构造函数的参数类型中定义的类型的所有出现都必须位于 严格正位置。如果某个位置不在函数的参数类型中（无论其周围嵌套了多少个函数类型），并且它不是除归纳类型的类型构造函数之外的任何表达式的参数，则该位置严格为正。此限制排除了不健全的归纳类型定义，但代价是也排除了一些没有问题的定义。

Non-strictly-positive inductive types

如果不拒绝，类型 Bad 将使 Lean 不一致：

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declaredinductive Bad where
  | bad : (Bad → Bad) → Bad

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared

这是因为可以编写一个循环论证，在假设 Bad 下证明 False。 Bad.bad 被拒绝，因为构造函数的参数的类型为 Bad → Bad，该类型是 Bad 作为参数类型出现的函数类型。

定点运算符的此声明被拒绝，因为 Fix 作为 f 的参数出现：

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declaredinductive Fix (f : Type u → Type u) where
  | fix : f (Fix f) → Fix f

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared

Fix.fix 被拒绝，因为 f 不是归纳类型的类型构造函数，但 Fix 本身作为它的参数出现。在这种情况下，Fix 也足以构造与 Bad 等效的类型：

def Bad : Type := Fix fun t => t → t

4.4.3.2.3. Prop 与 Type 对比🔗

Lean 拒绝实际上无法多态使用的全域多态类型。如果 Universe 参数的某些实例化导致类型本身成为 Prop，则可能会出现这种情况。如果此类型不是 subsingleton，则其递归器只能定位命题（即 motive 必须返回 Prop）。这些类型只有作为 Prop 本身才有意义，因此宇宙多态性可能是一个错误。由于它们基本上无用，因此 Lean 的归纳类型精化器并未设计为支持这些类型。

当这样的宇宙多态归纳类型确实是子单子时，定义它们是有意义的。 Lean 的标准库定义了 PUnit 和 PEmpty。要定义可以驻留在 Prop 或 Type 中的子单例，请将选项 bootstrap.inductiveCheckResultingUniverse 设置为 false。

option

bootstrap.inductiveCheckResultingUniverse

Default value: true

by default the inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into Prop. In the Init package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator

Overly-universe-polymorphic Bool

不允许定义可以在任何 Universe 中的 Bool 版本：

inductive PBool : Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort u

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`Sort u where
  | true
  | false

Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort u

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`

4.4.3.3. 终止检查的结构🔗

除了 Lean 的核心类型论为归纳类型规定的类型构造函数、构造函数和递归器之外，Lean 还构造了许多有用的帮助程序。首先，方程编译器（将模式匹配的递归函数转换为递归器的应用程序）使用这些附加构造：

recOn 是递归器的一个版本，其中每个构造函数的大前提先于小前提。
casesOn 是递归器的一个版本，其中每个构造函数的大前提先于小前提，并且递归参数不会产生归纳假设。它表达的是案例分析而不是原始递归。
below 计算一个类型，出于某种动机，表示归纳类型的所有居民（大前提的子树）满足该动机。它将归纳或原始递归的动机转变为强递归或强归纳的动机。
brecOn 是递归器的一个版本，其中 below 用于提供对所有子树的访问，而不仅仅是直接递归参数。它代表强感应。
noConfusion 是一个通用的陈述，从中可以导出构造函数的单射性和不相交性。
noConfusionType 是 noConfusion 的动机，它决定两个构造函数相等的结果。对于单独的构造函数，这是 False；如果两个构造函数相同，则结果是它们各自的参数相等。

这些结构遵循 McBride, Goguen, and McKinna (2004)Conor McBride, Healfdene Goguen, and James McKinna, 2004. “A Few Constructions on Constructors”. In Types for Proofs and Programs, International Workshop, TYPES 2004. (LNCS 3839) 中的描述。

对于良基递归，拥有可用的通用大小概念通常很有用。这是在 SizeOf 类中捕获的。

type class

SizeOf.{u} (α : Sort u) : Sort (max 1 u)
SizeOf.{u} (α : Sort u) : Sort (max 1 u)

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a "size" function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

Instance Constructor

SizeOf.mk.{u}

Methods

sizeOf : α → Nat

The "size" of an element, a natural number which decreases on fields of each inductive type.

4.4.4. 运行时表示🔗

归纳类型的运行时表示取决于它有多少个构造函数、每个构造函数采用多少个参数以及这些参数是否是相关。

4.4.4.1. 例外情况🔗

并非每个归纳类型都按此处所示表示 - 某些归纳类型具有 Lean 编译器的特殊支持：

固定位宽整数类型 UInt8、...、UInt64、Int8、...、Int64 和 USize 的表示形式取决于代码是针对 32 位架构还是针对 64 位架构进行编译。它们的表示被描述为在专门的部分中。
Char 由 uint32_t 表示。由于 Char 值不需要超过 21 位，因此它们始终未装箱。
Float 由指向包含“double”的 Lean 对象的指针表示。
至少有 2 个且至多有 2^{32} 个构造函数、并且每个构造函数均无参数的 枚举归纳 类型，由 uint8_t、uint16_t、uint32_t 中足以为每个构造函数分配唯一值的第一个类型表示。例如，类型 Bool 由 uint8_t 表示，其中值 0 代表 false，1 代表 true。
Decidable α 的表示方式与 Bool 相同。
Nat 和 Int 由 lean_object * 表示。它们的表示在关于自然数的部分和关于整数的部分中有更详细的描述。

4.4.4.2. 关联🔗

类型和证明没有运行时表示。也就是说，如果归纳类型是 Prop，则其值会在编译之前被擦除。同样，所有定理陈述和类型都被删除。具有运行时表示的类型称为 relevant，而没有运行时表示的类型称为 irrelevant。

Types are irrelevant

尽管 List.cons 具有以下签名，它指示三个参数：

List.cons.{u} {α : Type u} : α → List α → List α

它的运行时表示只有两个，因为类型参数与运行时无关。

Proofs are irrelevant

尽管 Fin.mk 具有以下签名，它指示三个参数：

Fin.mk {n : Nat} (val : Nat) : val < n → Fin n

它的运行时表示只有两个，因为证明被删除了。

在大多数情况下，不相关的值会从编译的代码中消失。但是，在需要某种表示的情况下（例如当它们是多态构造函数的参数时），它们由一个简单的值表示。

4.4.4.3. 简单的包装器🔗

如果归纳类型恰好具有一个构造函数，并且该构造函数恰好具有一个运行时相关参数，则归纳类型的表示方式与其参数相同。

Zero-Overhead Subtypes

结构 Subtype 将某种类型的元素与其满足谓词的证明捆绑在一起。它的构造函数有四个参数，但其中三个是不相关的：

Subtype.mk.{u} {α : Sort u} {p : α → Prop}
  (val : α) (property : p val) : Subtype p

因此，子类型不会在编译代码中产生运行时开销，并且与 val 字段的类型相同地表示。

Signed Integers

有符号整数类型 Int8、...、Int64、ISize 是具有单个字段的结构，该字段包装相应的无符号整数类型。它们分别由无符号 C 类型 uint8_t、...、uint64_t、size_t 表示，因为它们具有简单的结构。

4.4.4.4. 其他归纳类型🔗

如果归纳类型不属于上述类别之一，则其表示由其构造函数确定。没有相关参数的构造函数由它们在构造函数列表中的索引表示，作为未装箱的无符号机器整数（标量）。具有相关参数的构造函数表示为一个对象，该对象具有标头、构造函数的索引、指向其他对象的指针数组，然后是按其类型排序的标量字段数组。标头跟踪对象的引用计数和其他必要的簿记。

递归函数按照大多数编程语言的方式进行编译，而不是使用归纳类型的递归器。将递归函数细化为递归器可以提供可靠的终止证据，而不是可执行代码。

4.4.4.4.1. FFI🔗

从C的角度来看，这些其他的归纳类型都用lean_object *来表示。每个构造函数都存储为 lean_ctor_object，并且 lean_is_ctor 将返回 true。 lean_ctor_object 将构造函数索引存储在其标头中，字段存储在对象的 m_objs 部分中。 Lean 假设 sizeof(size_t) == sizeof(void*) — 虽然 C 不保证这一点，但 Lean 运行时系统包含一个断言，如果情况并非如此，该断言将失败。

字段的内存顺序源自声明中字段的类型和顺序。它们的顺序如下：

非标量字段存储为 lean_object *
USize 类型的字段
其他标量场，按大小降序排列

在每个组中，字段按声明顺序排序。警告：为此目的，普通包装类型被视为其基础包装类型。

要访问第一种字段，请使用 lean_ctor_get(val, i) 获取第 i 个非标量字段。
要访问 USize 字段，请使用 lean_ctor_get_usize(val, n+i) 获取第 i USize 字段，n 是第一类字段的总数。
要访问其他标量字段，请根据需要使用 lean_ctor_get_uintN(val, off) 或 lean_ctor_get_usize(val, off)。这里 off 是结构体中字段的字节偏移量，从 n*sizeof(void*) 开始，其中 n 是前两种字段的数量。

例如，如下结构

structure S where
  ptr_1 : Array Nat
  usize_1 : USize
  sc64_1 : UInt64
   -- Wrappers of scalars count as scalars:
  sc64_2 : { x : UInt64 // x > 0 }
  sc64_3 : Float -- `Float` is 64 bit
  sc8_1 : Bool
  sc16_1 : UInt16
  sc8_2 : UInt8
  sc64_4 : UInt64
  usize_2 : USize
  -- Trivial wrapper around `UInt32`
  sc32_1 : Char
  sc32_2 : UInt32
  sc16_2 : UInt16

将被重新排序为以下内存顺序：

S.ptr_1: lean_ctor_get(val, 0)
S.usize_1: lean_ctor_get_usize(val, 1)
S.usize_2: lean_ctor_get_usize(val, 2)
S.sc64_1: lean_ctor_get_uint64(val, sizeof(void*)*3)
S.sc64_2: lean_ctor_get_uint64(val, sizeof(void*)*3 + 8)
S.sc64_3: lean_ctor_get_float(val, sizeof(void*)*3 + 16)
S.sc64_4: lean_ctor_get_uint64(val, sizeof(void*)*3 + 24)
S.sc32_1: lean_ctor_get_uint32(val, sizeof(void*)*3 + 32)
S.sc32_2: lean_ctor_get_uint32(val, sizeof(void*)*3 + 36)
S.sc16_1: lean_ctor_get_uint16(val, sizeof(void*)*3 + 40)
S.sc16_2: lean_ctor_get_uint16(val, sizeof(void*)*3 + 42)
S.sc8_1: lean_ctor_get_uint8(val, sizeof(void*)*3 + 44)
S.sc8_2: lean_ctor_get_uint8(val, sizeof(void*)*3 + 45)

4.4.5. 相互归纳类型🔗

归纳类型可以相互递归。归纳类型的相互递归定义是通过定义 mutual ... end 块中的类型来指定的。

Mutually Defined Inductive Types

前面示例中的类型 EvenOddList 使用布尔索引来选择所讨论的列表是否应具有偶数或奇数个元素。这种区别也可以通过选择两个相互归纳类型EvenList 和 OddList 之一来表达：

mutual
  inductive EvenList (α : Type u) : Type u where
    | nil : EvenList α
    | cons : α → OddList α → EvenList α
  inductive OddList (α : Type u) : Type u where
    | cons : α → EvenList α → OddList α
end

example : EvenList String := .cons "x" (.cons "y" .nil)
example : OddList String := .cons "x" (.cons "y" (.cons "z" .nil))

example : OddList String := .cons "x" (.cons "y" Unknown constant `OddList.nil`

Note: Inferred this name from the expected resulting type of `.nil`:
  OddList String.nil)

Unknown constant `OddList.nil`

Note: Inferred this name from the expected resulting type of `.nil`:
  OddList String

Live ↪

4.4.5.1. 要求🔗

mutual 块中声明的归纳类型被视为一个组；它们必须共同满足非互递归归纳类型的格式良好标准的广义版本。即使可以在没有 mutual 块的情况下定义它们，情况也是如此，因为它们实际上不是相互递归的。

4.4.5.1.1. 相互依赖🔗

每个类型构造函数的签名必须能够在不引用 mutual 组中的其他归纳类型的情况下进行详细说明。换句话说，mutual组中的归纳类型不能互相作为参数。每个归纳类型的构造函数可以在其参数类型中提及组中的其他类型构造函数，其限制是非互归纳类型中递归出现的限制。

Mutual inductive type constructors may not mention each other

Lean 不接受这些归纳类型：

mutual
  inductive FreshList (α : Type) (r : α → α → Prop) : Type where
    | nil : FreshList α r
    | cons (x : α) (xs : FreshList α r) (fresh : Fresh r x xs)
  Invalid mutually inductive types: Binder annotations for parameter `α` must matchinductive Fresh
      (r : α → Unknown identifier `FreshList`FreshList α → Prop) :
      α → Unknown identifier `FreshList`FreshList α r → Prop where
    | nil : Fresh r x .nil
    | cons : r x y → (f : Fresh r x ys) → Fresh r x (.cons y ys f)
end

类型构造函数可能不引用 mutual 组中的其他类型构造函数，因此 FreshList 不在 Fresh 的类型构造函数的范围内：

Unknown identifier `FreshList`

4.4.5.1.2. 参数必须匹配🔗

mutual 组中的所有归纳类型必须具有相同的参数。它们的指数可能不同。

Differing numbers of parameters

尽管 Both 和 OneOf 不是相互递归的，但它们是在同一 mutual 块中声明的，因此必须具有相同的参数：

mutual
  inductive Both (α : Type u) (β : Type v) where
    | mk : α → β → Both α β
  Invalid mutually inductive types: `Optional` has 1 parameter(s), but the preceding type `Both` has 2

Note: All inductive types declared in the same `mutual` block must have the same parametersinductive Optional (α : Type u) where
    | none
    | some : α → Optional α
end

Invalid mutually inductive types: `Optional` has 1 parameter(s), but the preceding type `Both` has 2

Note: All inductive types declared in the same `mutual` block must have the same parameters

Differing parameter types

尽管 Many 和 OneOf 不是相互递归的，但它们是在同一 mutual 块中声明的，因此必须具有相同的参数。它们都只有一个参数，但 Many 的参数不一定与 Optional 的参数位于同一宇宙中：

mutual
  inductive Many (α : Type) : Type u where
    | nil : Many α
    | cons : α → Many α → Many α
  Invalid mutually inductive types: Parameter `α` has type
  Type u
of sort `Type (u + 1)` but is expected to have type
  Type
of sort `Type 1`inductive Optional (α : Type u) where
    | none
    | some : α → Optional α
end

Invalid mutually inductive types: Parameter `α` has type
  Type u
of sort `Type (u + 1)` but is expected to have type
  Type
of sort `Type 1`

4.4.5.1.3. 宇宙层级🔗

相互组中每个归纳类型的宇宙层级必须遵守与非相互递归归纳类型相同的要求。此外，共同组中的所有归纳类型必须位于同一宇宙中，这意味着它们的构造函数在其参数的宇宙方面同样受到限制。

Universe mismatch

这些相互归纳类型是表示列表的游程长度编码的一种有点复杂的方法：

mutual
  inductive RLE : List α → Type where
  | nil : RLE []
  | run (x : α) (n : Nat) :
    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs

  inductive PrefixRunOf : Nat → α → List α → List α → Type where
  | zero
    (noMore : ¬∃zs, xs = x :: zs := by simp) :
    PrefixRunOf 0 x xs xs
  | succ :
    PrefixRunOf n x xs ys →
    PrefixRunOf (n + 1) x (x :: xs) ys
end

example : RLE [1, 1, 2, 2, 3, 1, 1, 1] :=
  .run 1 2 (by⊢ 2 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ .zero)) <|
  .run 2 2 (by⊢ 2 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ .zero)) <|
  .run 3 1 (by⊢ 1 ≠ 0 decideAll goals completed! 🐙) (.succ .zero) <|
  .run 1 3 (by⊢ 3 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ (.succ (.zero)))) <|
  .nil

将 PrefixRunOf 指定为 Prop 是明智的，但这是不可能的，因为这些类型将位于不同的 Universe 中：

mutual
  inductive RLE : List α → Type where
  | nil : RLE []
  | run
    (x : α) (n : Nat) :
    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys →
    RLE xs

  Invalid mutually inductive types: The resulting type of this declaration
  Prop
differs from a preceding one
  Type

Note: All inductive types declared in the same `mutual` block must belong to the same type universeinductive PrefixRunOf : Nat → α → List α → List α → Prop where
  | zero
    (noMore : ¬∃zs, xs = x :: zs := by simp) :
    PrefixRunOf 0 x xs xs
  | succ :
    PrefixRunOf n x xs ys →
    PrefixRunOf (n + 1) x (x :: xs) ys
end

Invalid mutually inductive types: The resulting type of this declaration
  Prop
differs from a preceding one
  Type

Note: All inductive types declared in the same `mutual` block must belong to the same type universe

这个特殊的属性可以通过单独定义格式良好条件并使用子类型来表达：

def RunLengths α := List (α × Nat)
def NoRepeats : RunLengths α → Prop
  | [] => True
  | [_] => True
  | (x, _) :: ((y, n) :: xs) =>
    x ≠ y ∧ NoRepeats ((y, n) :: xs)
def RunsMatch : RunLengths α → List α → Prop
  | [], [] => True
  | (x, n) :: xs, ys =>
    ys.take n = List.replicate n x ∧
    RunsMatch xs (ys.drop n)
  | _, _ => False
def NonZero : RunLengths α → Prop
  | [] => True
  | (_, n) :: xs => n ≠ 0 ∧ NonZero xs
structure RLE (xs : List α) where
  rle : RunLengths α
  noRepeats : NoRepeats rle
  runsMatch : RunsMatch rle xs
  nonZero : NonZero rle

example : RLE [1, 1, 2, 2, 3, 1, 1, 1] where
  rle := [(1, 2), (2, 2), (3, 1), (1, 3)]
  noRepeats := by⊢ NoRepeats [(1, 2), (2, 2), (3, 1), (1, 3)] simp [NoRepeats]All goals completed! 🐙
  runsMatch := by⊢ RunsMatch [(1, 2), (2, 2), (3, 1), (1, 3)] [1, 1, 2, 2, 3, 1, 1, 1] simp [RunsMatch]All goals completed! 🐙
  nonZero := by⊢ NonZero [(1, 2), (2, 2), (3, 1), (1, 3)] simp [NonZero]All goals completed! 🐙

4.4.5.1.4. 积极性🔗

mutual 组中定义的每个归纳类型只能严格正向出现在该组中所有类型的构造函数的参数类型中。换句话说，在该组的所有类型中每个构造函数的每个参数的类型中，该组中的任何类型构造函数都不会出现在任何箭头的左侧，并且它们都不会出现在参数位置，除非它们是归纳类型的类型构造函数的参数。

Mutual strict positivity

在以下共同组中，Tm 出现在 Binding.scope 参数中的负位置：

mutual
  (kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declaredinductive Tm where
    | app : Tm → Tm → Tm
    | lam : Binding → Tm
  inductive Binding where
    | scope : (Tm → Tm) → Binding
end

由于 Tm 是同一共同组的一部分，因此它只能严格正数出现在 Binding 构造函数的参数中。然而，它的发生却是消极的：

(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared

Nested positions

LocatedStx 和 Stx 的定义满足正性条件，因为递归出现不在任何箭头的左侧，并且当它们是参数时，它们是归纳类型构造函数的参数。

mutual
  inductive LocatedStx where
    | mk (line col : Nat) (val : Stx)
  inductive Stx where
    | atom (str : String)
    | node (kind : String) (args : List LocatedStx)
end

Live ↪

4.4.5.2. 递归器🔗

相互的归纳类型提供有原始递归器，就像非相互定义的归纳类型一样。这些递归器考虑到它们必须处理组中的其他类型，因此每个归纳类型都有一个动机。由于 mutual 组中的所有归纳类型都需要具有相同的参数，因此递归器仍然首先采用参数，将它们抽象到动机和递归器的其余部分。此外，由于递归程序必须处理组的其他类型，因此需要为组中每种类型的每个构造函数提供案例。不考虑类型之间的实际依赖结构；即使由于相互依赖性较少而实际上并不需要额外的动机或构造函数，生成的递归器仍然需要它们。

Even and odd

mutual
  inductive Even : Nat → Prop where
    | zero : Even 0
    | succ : Odd n → Even (n + 1)
  inductive Odd : Nat → Prop where
    | succ : Even n → Odd (n + 1)
end

Even.rec
  {motive_1 : (a : Nat) → Even a → Prop}
  {motive_2 : (a : Nat) → Odd a → Prop}
  (zero : motive_1 0 Even.zero)
  (succ : {n : Nat} → (a : Odd n) → motive_2 n a → motive_1 (n + 1) (Even.succ a)) :
  (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) →
  ∀ {a : Nat} (t : Even a), motive_1 a t

Odd.rec
  {motive_1 : (a : Nat) → Even a → Prop}
  {motive_2 : (a : Nat) → Odd a → Prop}
  (zero : motive_1 0 Even.zero)
  (succ : ∀ {n : Nat} (a : Odd n), motive_2 n a → motive_1 (n + 1) (Even.succ a)) :
  (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) → ∀ {a : Nat} (t : Odd a), motive_2 a t

Live ↪

Spuriously mutual types

类型 Two 和 Three 在共同块中定义，即使它们不互相引用：

mutual
  inductive Two (α : Type) where
    | mk : α → α → Two α
  inductive Three (α : Type) where
    | mk : α → α → α → Three α
end

尽管如此，Two 的递归器 Two.rec 仍然需要 Three 的动机和案例：

Two.rec.{u} {α : Type}
  {motive_1 : Two α → Sort u}
  {motive_2 : Three α → Sort u}
  (mk : (a a_1 : α) → motive_1 (Two.mk a a_1)) :
  ((a a_1 a_2 : α) → motive_2 (Three.mk a a_1 a_2)) → (t : Two α) → motive_1 t

Live ↪

4.4.5.3. 运行时表示🔗

相互归纳类型在编译代码和运行时中的表示方式与非相互归纳类型相同。对相互归纳类型的限制的存在是为了确保 Lean 作为逻辑的一致性，并且不影响编译的代码。

4.4.5.4. 嵌套归纳类型🔗

嵌套归纳类型是归纳类型，其中所定义的类型的递归出现是其他归纳类型构造函数的参数。这些递归出现“嵌套”在其他类型构造函数的下面。满足一定要求的嵌套归纳类型可以转化为相互的归纳类型；这个翻译表明它们是合理的。在内部，内核执行此转换；如果成功，则接受原始嵌套的归纳类型。这避免了翻译表面细节可能引起的性能和可用性问题。

嵌套递归出现必须满足以下要求：

它们必须直接嵌套在归纳类型的类型构造函数下。不接受减少此类嵌套出现的术语。
局部变量（例如构造函数的参数）可能不会出现在嵌套出现的参数中。
嵌套事件必须严格正向发生。它们必须严格出现在它们嵌套的位置，并且它们嵌套的类型构造函数本身也必须出现在严格的正位置。
类型包含嵌套出现的构造函数参数不能以依赖于外部类型构造函数的特定选择的方式使用。翻译后的版本将无法在这些情况下使用。
嵌套出现不能用作外部类型索引类型中出现的外部类型构造函数的参数。

Nested Inductive Types

可以使用 Option 定义自然数，而不是使用两个构造函数：

inductive ONat : Type where
  | mk (pred : Option ONat)

任意分支树，也称为玫瑰树，嵌套归纳类型：

inductive RTree (α : Type u) : Type u where
  | empty
  | node (val : α) (children : List (RTree α))

Live ↪

Invalid Nested Inductive Types

这个任意分支玫瑰树的声明声明了 List 的别名，而不是直接使用 List：

abbrev Children := List

(kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declaredinductive RTree (α : Type u) : Type u where
  | empty
  | node (val : α) (children : Children (RTree α))

(kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declared

任意分支玫瑰树的声明使用索引跟踪树的深度。构造函数 DRTree.node 有一个自动隐式参数 n，表示所有子树的深度。但是，局部变量（例如构造函数参数）不允许作为嵌套出现的参数：

(kernel) invalid nested inductive datatype 'List', nested inductive datatypes parameters cannot contain local variables.inductive DRTree (α : Type u) : Nat → Type u where
  | empty : DRTree α 0
  | node (val : α) (children : List (DRTree α n)) : DRTree α (n + 1)

此声明包括嵌套在 Option 下的归纳类型的非严格正数出现：

(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declaredinductive WithCheck where
  | done
  | check (f : Option WithCheck → Bool)

(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declared

这棵玫瑰树的分支因子受其参数限制：

(kernel) application type mismatch
  List.length children
argument has type
  @_nested.List_1 branches α
but function has type
  List (@BRTree branches α) → Natinductive BRTree (branches : Nat) (α : Type u) : Type u where
  | mk :
    (children : List (BRTree branches α)) →
    children.length < branches →
    BRTree branches α

仅允许可转换为相互归纳类型的嵌套归纳类型。但是，转换此类型需要将 List.length 转换为已转换类型，但函数定义可能不会出现在与归纳类型的交互块中。生成的错误消息表明该函数未翻译，但应用于翻译类型的术语：

(kernel) application type mismatch
  List.length children
argument has type
  @_nested.List_1 branches α
but function has type
  List (@BRTree branches α) → Nat

可以将参数与完全多态函数的嵌套出现一起使用，例如 id：

inductive Variable name `RTree''` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`RTree'' (α : Type u) : Type u where
  | mk :
    (children : List (BRTree branches α)) →
    id children = children →
    BRTree branches α

在这种情况下，该函数同样适用于翻译版本和原始版本。

palindrome 是颠倒后相同的列表：

inductive Palindrome (α : Type) : List α → Prop where
  | nil : Palindrome α []
  | single : Palindrome α [x]
  | cons (x : α) (p : Palindrome α xs) : Palindrome α (x :: xs ++ [x])

在这个谓词中，列表是一个索引，其类型取决于参数，为了清楚起见，参数是显式的。这意味着它无法使用

从嵌套归纳类型到相互归纳类型的转换过程如下：

嵌套出现变为归纳类型: 归纳类型的嵌套出现被转换为同一共同组中的新归纳类型，从而替换原始的嵌套出现。这些新的归纳类型具有与外部归纳类型相同的构造函数，只是原始参数由类型的翻译版本实例化。原始归纳类型成为嵌套出现已被重写的版本的别名。如果结果类型也是嵌套的归纳类型（例如，嵌套在 Array 下的类型变为嵌套在 List 下的类型，因为 Array 的构造函数采用 List），则重复此过程。
与嵌套类型之间的转换: 生成应用于新别名的外部归纳类型与生成的辅助类型之间的转换。然后证明这些转换是互逆的。
构造函数重构: 原始类型的每个构造函数都被定义为一个函数，该函数在应用适当的转换后返回翻译类型的构造函数。
递归重构: 嵌套归纳类型的递归器是根据转换类型的递归器构造的。在翻译中，嵌套事件的动机由转换函数组成，小前提根据需要使用它们。需要证明转换函数互逆，因为编码的构造函数在一个方向上进行转换，但最终应用于另一个方向上的转换结果。

Translating Nested Inductive Types

此嵌套归纳类型代表自然数：

inductive ONat where
  | mk (pred : Option ONat) : ONat

ONat.rec.{u} {motive_1 : ONat → Sort u} {motive_2 : Option ONat → Sort u}
  (mk : (pred : Option ONat) → motive_2 pred → motive_1 (ONat.mk pred)) (none : motive_2 none)
  (some : (val : ONat) → motive_1 val → motive_2 (some val)) (t : ONat) : motive_1 t#check ONat.rec

内部转换的第一步是用“内联”结果类型的辅助归纳类型替换嵌套出现的情况。在本例中，嵌套出现位于 Option 下；因此，辅助类型具有 Option 的构造函数，并用 ONat' 替换类型参数：

mutual
inductive ONat' where
  | mk (pred : OptONat) : ONat'

inductive OptONat where
  | none
  | some : ONat' → OptONat
end

ONat' 是 ONat 的编码：

def ONat := ONat'

下一步是定义转换函数，将原始嵌套类型与辅助类型相互转换：

def OptONat.ofOption : Option ONat → OptONat
  | Option.none => OptONat.none
  | Option.some o => OptONat.some o
def OptONat.toOption : OptONat → Option ONat
  | OptONat.none => Option.none
  | OptONat.some o => Option.some o

这些转换函数是互逆的：

def OptONat.to_of_eq_id o :
    OptONat.toOption (ofOption o) = o := byo:Option ONat⊢ (ofOption o).toOption = o
  cases onone⊢ (ofOption Option.none).toOption = Option.nonesomeval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ <;>none⊢ (ofOption Option.none).toOption = Option.nonesomeval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ rflAll goals completed! 🐙
def OptONat.of_to_eq_id o :
    OptONat.ofOption (OptONat.toOption o) = o := byo:OptONat⊢ ofOption o.toOption = o
  cases onone⊢ ofOption none.toOption = nonesomea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ <;>none⊢ ofOption none.toOption = nonesomea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ rflAll goals completed! 🐙

原始构造函数被转换为翻译对应构造函数的应用程序，并对嵌套出现应用适当的转换：

def ONat.mk (pred : Option ONat) : ONat :=
  ONat'.mk (.ofOption pred)

最后，可以翻译原始类型的递归器。翻译后的递归器使用翻译后类型的递归器。原始嵌套出现使用转换进行翻译，并且转换互逆的证明用于根据需要重写类型。

noncomputable def ONat.rec
    {motive1 : ONat → Sort u}
    {motive2 : Option ONat → Sort u}
    (h1 :
      (pred : Option ONat) → motive2 pred →
      motive1 (ONat.mk pred))
    (h2 : motive2 none)
    (h3 : (o : ONat) → motive1 o → motive2 (some o)) :
    (t : ONat) → motive1 t :=
  @ONat'.rec motive1 (motive2 ∘ OptONat.toOption)
    (fun pred ih =>
      OptONat.of_to_eq_id pred ▸ h1 pred.toOption ih)
    h2
    h3

Live ↪

4.4.5.5. 格理论归纳和共归纳谓词🔗

归纳类型声明的语法可用于指定归纳谓词和共归纳谓词。这些不是 Lean 类型系统的内置功能，而是精心设计成合适的编码。它们在专用部分中进行了描述。

4.1.	功能
4.2.	提案
4.3.	宇宙
4.4.	归纳类型
4.5.	商数