本文深入介绍了Lean 4编程语言中的结构体概念及其应用。结构体允许程序员定义包含多个字段的数据类型，并通过构造函数创建实例。文章通过实例展示了如何定义结构体、创建结构体实例（包括使用默认和自定义构造函数），以及结构体继承的用法。此外，还探讨了如何在结构体中定义函数，并分析了Lean 4中基本数据类型（如Float、Char、UInt32等）的底层实现，揭示了它们实际上也是结构体或依赖于结构体。最后，详细讲解了字符串在Lean 4中的表示和处理方式，包括编码问题和字符访问。

🧱 结构体的定义与实例化：Lean 4 使用 `structure` 关键字定义结构体，可以包含多个字段，并通过 `结构体名.mk` 自动生成默认构造函数，或者自定义构造函数。例如，`HeavenlyStem` 结构体包含 `name`、`element` 和 `yinYang` 字段，可以使用 `{ 字段名 := 值, ... }` 或 `HeavenlyStem.mk` 两种方式创建实例。

🧬 结构体的继承与扩展：Lean 4 允许结构体继承自其他结构体，从而获得父结构体的字段和方法。`Point3D` 结构体通过 `extends Point` 继承了 `Point` 结构体的 `x` 和 `y` 坐标，并新增了 `z` 坐标，实现了对 2D 点的扩展。

🧮 结构体中的函数定义与调用：函数可以作为结构体的成员，直接在结构体内部定义，也可以在外部定义并与结构体关联。例如，`Point` 结构体内部定义了 `distanceToOrigin` 函数，外部定义了 `manhattanDistanceToOrigin` 函数，都可以通过 `实例名.函数名` 的方式调用。

🧩 Lean 4 基本类型的结构体本质：Lean 4 中的许多基本类型，如 `Float`、`Char`、`UInt32` 等，实际上都是结构体。例如，`Float` 类型是一个包含 `val` 字段的结构体，`Char` 类型包含 `val` 和 `valid` 字段，这体现了 Lean 4 中结构体的重要性和广泛应用。

✍️ 字符串的表示与处理：Lean 4 中的字符串是一个结构体，包含一个字符列表 `data`。文章讲解了字符串的编码问题（UTF-8）以及如何获取字符串的长度（字节数而非字符数），如何将字符串转换为字符列表，以及如何使用 `get` 和 `next` 函数访问字符串中的字符。

面向程序员的Lean 4教程(4) - 结构体结构体也是程序员们的老朋友了，它的作用是定义一个数据类型，并给这个数据类型定义一些字段。结构体在Lean中，结构体使用structure关键字定义。structure Point where x : Nat y : NatLean 4 会为结构体自动生成默认构造函数，名称是 结构体名.mk。也可以通过定义函数来自定义构造函数。使用 { 字段名 := 值, ... } 的语法可以更方便地创建结构体实例。我们来看一个例子：-- 定义五行枚举类型inductive FiveElement : Type where | Wood -- 木 | Fire -- 火 | Earth -- 土 | Metal -- 金 | Water -- 水 deriving Repr-- 为 FiveElement 定义 ToString 实例instance : ToString FiveElement where toString | FiveElement.Wood => "木" | FiveElement.Fire => "火" | FiveElement.Earth => "土" | FiveElement.Metal => "金" | FiveElement.Water => "水"-- 定义阴阳枚举类型inductive YinYang : Type where | Yin -- 阴 | Yang -- 阳 deriving Repr-- 为 YinYang 定义 ToString 实例instance : ToString YinYang where toString | YinYang.Yin => "阴" | YinYang.Yang => "阳"-- 定义天干结构体structure HeavenlyStem where name : String -- 天干名称 element : FiveElement -- 五行属性 yinYang : YinYang -- 阴阳属性 deriving Repr我们来看两种创建结构体实例的方法：def jia : HeavenlyStem := { name := "甲", element := FiveElement.Wood, yinYang := YinYang.Yang }def yi : HeavenlyStem := HeavenlyStem.mk "乙" FiveElement.Wood YinYang.Yin结构体的继承结构体可以继承另一个结构体，从而获得父结构体的字段和方法。比如，我们可以为2D的点添加z坐标，从而获得3D的点。structure Point where x : Float y : Float deriving Reprstructure Point3D extends Point where z : Float deriving Reprdef redPoint : Point3D := { x := 1.0, y := 2.0, z := 3.0 }#eval redPoint.x -- 输出: 1.0#eval redPoint.y -- 输出: 2.0#eval redPoint.z -- 输出: 3.0def point2d : Point := { x := 0.0, y := 0.0 }def point3d : Point3D := { point2d with z := 4.0 }#eval point3d -- 输出: { x := 0.0, y := 0.0, z := 4.0 }函数是Lean4中的一等公民，自然也可以是结构体的一部分。structure Point where x : Float y : Float distanceToOrigin : Float := Float.sqrt (x x + y y) deriving Repr定义在结构体的外面也不影响使用，比如我们给点增加一个计算曼哈顿距离的函数。def Point.manhattanDistanceToOrigin (p : Point) : Float := Float.abs p.x + Float.abs p.y调用方法是一样的：#eval point2d.distanceToOrigin -- 输出: 5.0#eval point2d.manhattanDistanceToOrigin -- 输出: 7.0伪装成基本类型的结构体上一节我们学习了一些伪装成基本类型的归纳类型。还有一些基本类型没有介绍到，其实它们都是伪装成基本类型的结构体。我们先看看Float类型：info: ....\Test3\Basic.lean:47:0: structure Float : Typenumber of parameters: 0fields: Float.val : floatSpec.floatconstructor: Float.mk (val : floatSpec.float) : FloatFloat类型是一个结构体，它有一个字段val，类型是floatSpec.float。FloatSpec又是个啥呢，还是个结构体：structure FloatSpec where float : Type val : float lt : float → float → Prop le : float → float → Prop decLt : DecidableRel lt decLe : DecidableRel leval是float类型，而float是Type类型。这是根据系统不同定义的类型，总之是符合IEEE 754标准的浮点数。我们再来看字符Char类型：info: ....\Test3\Basic.lean:57:0: structure Char : Typenumber of parameters: 0fields: Char.val : UInt32 Char.valid : self.val.isValidCharconstructor: Char.mk (val : UInt32) (valid : val.isValidChar) : CharChar类型是一个结构体，它有一个字段val，类型是UInt32。isValidChar是一个函数，用于判断val是否是一个有效的字符。我们再来看UInt32类型：info: ....\Test3\Basic.lean:53:0: structure UInt32 : Typenumber of parameters: 0fields: UInt32.toBitVec : BitVec 32constructor: UInt32.mk (toBitVec : BitVec 32) : UInt32UInt32类型也是一个结构体，它有一个字段toBitVec，类型是BitVec 32。注意，这是一个类型依赖。类型不是BitVec，而是依赖于后面的值的类型。用人话就说就是，不同长度的BitVec不是同一个类型。info: ....\Test3\Basic.lean:73:0: structure BitVec (w : Nat) : Typenumber of parameters: 1fields: BitVec.toFin : Fin (2 ^ w)constructor: BitVec.ofFin {w : Nat} (toFin : Fin (2 ^ w)) : BitVec w这也是我们明明要讲基本数据类型，但是上一节要讲类型依赖的原因。很多语言中非常基础的类型，在Lean中要么是归纳类型，要么是结构体，甚至有些还是类型依赖的类型。同理，UInt8, UInt16, UInt64也都是依赖不同长度的BitVec。info: ....\Test3\Basic.lean:49:0: structure UInt8 : Typenumber of parameters: 0fields: UInt8.toBitVec : BitVec 8constructor: UInt8.mk (toBitVec : BitVec 8) : UInt8info: ....\Test3\Basic.lean:51:0: structure UInt16 : Typenumber of parameters: 0fields: UInt16.toBitVec : BitVec 16constructor: UInt16.mk (toBitVec : BitVec 16) : UInt16info: ....\Test3\Basic.lean:53:0: structure UInt32 : Typenumber of parameters: 0fields: UInt32.toBitVec : BitVec 32constructor: UInt32.mk (toBitVec : BitVec 32) : UInt32info: ....\Test3\Basic.lean:55:0: structure UInt64 : Typenumber of parameters: 0fields: UInt64.toBitVec : BitVec 64constructor: UInt64.mk (toBitVec : BitVec 64) : UInt64与List是个归纳类型不同，Array是个结构体。info: ....\Test3\Basic.lean:61:0: structure Array.{u} (α : Type u) : Type unumber of parameters: 1fields: Array.toList : List αconstructor: Array.mk.{u} {α : Type u} (toList : List α) : Array α另外，Lean4中还有向量Vector，它继承自Array，但是依赖于长度，每一种长度的Vector是不同的类型。info: ....\Test3\Basic.lean:77:0: structure Vector.{u} (α : Type u) (n : Nat) : Type unumber of parameters: 2parents: Vector.toArray : Array αfields: Array.toList : List α Vector.size_toArray : self.size = nconstructor: Vector.mk.{u} {α : Type u} {n : Nat} (toArray : Array α) (size_toArray : toArray.size = n) : Vector α nresolution order: Vector, Array定长的向量和有限的有理数都是类型依赖的经典例子。字符串最后，字符串还需要单独拿出来说一下。字符串是一个结构体，只有一个字段是字符的列表。info: ....\Test3\Basic.lean:63:0: structure String : Typenumber of parameters: 0fields: String.data : List Charconstructor: String.mk (data : List Char) : String但是因为不定长字符编码的问题，字符串的长度远比字符列表的长度要复杂。首先，如果你是在Windows系统上运行Lean 4，可能会遇到显示中文乱码的问题。这是因为Windows默认使用GBK编码，而Lean 4使用的是UTF-8编码。我们可以通过修改控制台的代码页为 UTF-8（代码页 65001）来支持 UTF-8 字符串的输出。chcp 65001在 Lean 4 中，字符串是 Unicode 字符的序列。字符串字面量使用双引号括起来。我们仍然使用lenght函数来获取字符串的长度。 let s10 := "数学世界666" IO.println s10 let n10 := s10.length IO.println n10运行结果如下：数学世界6667我们知道，utf-8编码的中文字符占用超过一个字节，字符串长度取7并不是按照字符个数计算的。我们可以使用toUTF8函数来将其转换成字节数组，然后计算这个ByteArray的长度： let n11 := s10.toUTF8.size IO.println n11我们可以看到，这个字符串占用了15个字节。字符串的每个字符都是Unicode字符，所以我们可以使用toList函数将其转换成字符列表，然后使用get函数获取每个字符。 let slist := s10.toList IO.println slist let c01 := slist[0] IO.println c01 let c02 := slist[1] IO.println c02 let c03 := slist[2] IO.println c03输出如下：[数, 学, 世, 界, 6, 6, 6] 数 学 世 但是，如果你使用get函数获取字符串中的字符，你会发现它需要的是一个String.Pos类型。在起点的时候还好办，Lean4会自动推断出起点是0。 let startPos : String.Pos := 0 let c000 := s10.get startPos IO.println c000但是，如果你想要获取下一个字符，就需要使用next函数来获取下一个位置： let nextPos : String.Pos := s10.next startPos let c001 := s10.get nextPos IO.println c001 let nextPos2 : String.Pos := s10.next nextPos let c002 := s10.get nextPos2 IO.println c002输出如下：数学世小结这一节我们学习了结构体，通过结构体，可以定义变量，也可以定义函数，还可以通过继承来扩展结构体。同时，通过对于基本类型的分析，我们发现了归纳类型和类型依赖在Lean4中的重要性。