跳到主要内容

Lean 数组

数组是编程中最基础且常用的数据结构之一。在Lean编程语言中，数组是一种有序的元素集合，允许通过索引快速访问和修改元素。本文将详细介绍Lean数组的概念、基本操作以及实际应用场景。

什么是数组？​

数组是一种线性数据结构，用于存储相同类型的元素。每个元素在数组中都有一个唯一的索引，通常从0开始。数组的大小在创建时确定，且不可更改。

数组的特点​

  • 有序性：数组中的元素按顺序存储。
  • 索引访问：通过索引可以快速访问数组中的元素。
  • 固定大小：数组的大小在创建时确定，不可动态调整。

Lean 数组的基本操作​

创建数组​

在Lean中，可以使用以下语法创建一个数组：

lean
def myArray : Array Nat := #[1, 2, 3, 4, 5]

这里，myArray 是一个包含5个自然数的数组。

访问数组元素​

可以通过索引访问数组中的元素。Lean中的数组索引从0开始：

lean
#eval myArray[0]  -- 输出: 1
#eval myArray[2]  -- 输出: 3

修改数组元素​

Lean数组是不可变的，这意味着一旦创建，就不能直接修改数组中的元素。但可以通过创建新数组来实现类似的效果：

lean
def newArray := myArray.set 1 10
#eval newArray  -- 输出: #[1, 10, 3, 4, 5]

数组的长度​

可以使用 size 方法获取数组的长度：

lean
#eval myArray.size  -- 输出: 5

实际应用场景​

案例1：计算数组元素的和​

假设我们需要计算一个数组中所有元素的和，可以使用以下代码：

lean
def sumArray (arr : Array Nat) : Nat :=
  arr.foldl (fun acc x => acc + x) 0

#eval sumArray myArray  -- 输出: 15

案例2：查找数组中的最大值​

我们可以编写一个函数来查找数组中的最大值：

lean
def maxArray (arr : Array Nat) : Nat :=
  arr.foldl (fun acc x => if x > acc then x else acc) 0

#eval maxArray myArray  -- 输出: 5

总结​

数组是Lean编程语言中非常基础且重要的数据结构。通过本文，我们学习了如何创建、访问和修改数组，以及如何在实际应用中使用数组。掌握数组的基本操作是学习更复杂数据结构的基础。

附加资源与练习​

  • 练习1：编写一个函数，计算数组中所有元素的平均值。
  • 练习2：编写一个函数，将两个数组合并为一个新数组。
  • 练习3：编写一个函数，判断数组中是否存在某个特定元素。
提示

建议初学者通过实际编写代码来加深对数组的理解。尝试完成上述练习，并在Lean环境中运行你的代码。