在 Lean 中，模式匹配可用于串联空值检查。 从列表中取得第一个条目可以直接使用可选索引记法：

def first (xs : List α) : Option α := xs[0]?

结果必须是 Option，因为空列表没有第一个条目。 提取第一个和第三个条目需要检查每一个都不是 none：

def firstThird (xs : List α) : Option (α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => some (first, third)

类似地，提取第一、第三和第五个条目需要进行更多检查，以确保这些值不是 none：

def firstThirdFifth (xs : List α) : Option (α × α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => match xs[4]? with | none => none | some fifth => some (first, third, fifth)

而向这个序列添加第七个条目开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => match xs[4]? with | none => none | some fifth => match xs[6]? with | none => none | some seventh => some (first, third, fifth, seventh)

这段代码的根本问题在于它处理了两个关注点：提取这些数字，以及检查它们是否全部存在。 第二个关注点是通过复制并粘贴处理 none 情形的代码来解决的。 通常，将重复的片段提升为辅助函数是一种良好的风格：

def andThen (opt : Option α) (next : α → Option β) : Option β := match opt with | none => none | some x => next x

这个辅助函数的用法类似于 C# 和 Kotlin 中的 ?.，它负责传播 none 值。 它接受两个参数：一个可选值，以及一个在该值不是 none 时应用的函数。 如果第一个参数是 none，则该辅助函数返回 none。 如果第一个参数不是 none，则将该函数应用于 some 构造子的内容。

现在，firstThird 可以改写为使用 andThen 而不是模式匹配：

def firstThird (xs : List α) : Option (α × α) := andThen xs[0]? fun first => andThen xs[2]? fun third => some (first, third)

在 Lean 中，函数作为参数传递时不需要用括号括起来。 下面这个等价定义使用了更多括号，并缩进了函数体：

def firstThird (xs : List α) : Option (α × α) := andThen xs[0]? (fun first => andThen xs[2]? (fun third => some (first, third)))

andThen 辅助函数提供了一种让值流经其中的“管道”，而带有略显不同寻常缩进的版本更能暗示这一点。 改进用于编写 andThen 的语法，可以使这些计算更易理解。

这通常通过定义一种既可以是错误也可以是结果的数据类型，并将带异常的函数翻译为返回该数据类型的函数来完成：

inductive Except (ε : Type) (α : Type) where | error : ε → Except ε α | ok : α → Except ε α deriving BEq, Hashable, Repr

类型变量 ε 表示该函数可能产生的错误的类型。 调用者应当同时处理错误和成功，这使得类型变量 ε 所起的作用有点类似于 Java 中受检异常列表的作用。

与 Option 类似，Except 可以用来表示未能在列表中找到某个条目。 在这种情况下，错误类型是 String：

def get (xs : List α) (i : Nat) : Except String α := match xs[i]? with | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})" | some x => Except.ok x

查找一个在界内的值会得到一个 Except.ok：

def ediblePlants : List String := ["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]Except.ok "sea buckthorn"#eval get ediblePlants 2

Except.ok "sea buckthorn"

查找越界值会产生一个 Except.error：

Except.error "Index 4 not found (maximum is 3)"#eval get ediblePlants 4

Except.error "Index 4 not found (maximum is 3)"

一次列表查找可以方便地返回一个值或一个错误：

def first (xs : List α) : Except String α := get xs 0

然而，执行两次列表查找需要处理潜在的失败：

def firstThird (xs : List α) : Except String (α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => Except.ok (first, third)

向该函数添加另一次列表查找需要更多的错误处理：

def firstThirdFifth (xs : List α) : Except String (α × α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => match get xs 4 with | Except.error msg => Except.error msg | Except.ok fifth => Except.ok (first, third, fifth)

再增加一次列表查找后，情况开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => match get xs 4 with | Except.error msg => Except.error msg | Except.ok fifth => match get xs 6 with | Except.error msg => Except.error msg | Except.ok seventh => Except.ok (first, third, fifth, seventh)

再一次，可以将一种常见模式分解出来作为辅助函数。 函数中的每一步都会检查是否有错误，并且只有当结果为成功时，才继续进行其余计算。 可以为 Except 定义 andThen 的一个新版本：

def andThen (attempt : Except e α) (next : α → Except e β) : Except e β := match attempt with | Except.error msg => Except.error msg | Except.ok x => next x

正如 Option 的情形一样，这个 andThen 版本允许对 firstThird' 作出更简洁的定义：

def firstThird' (xs : List α) : Except String (α × α) := andThen (get xs 0) fun first => andThen (get xs 2) fun third => Except.ok (first, third)

在 Option 和 Except 两种情形中，都有两个重复出现的模式：一是在每一步检查中间结果，这已经被分解到 andThen 中；二是最终的成功结果，分别是 some 或 Except.ok。 为方便起见，可以将成功分解到一个名为 ok 的辅助函数中：

def ok (x : α) : Except ε α := Except.ok x

类似地，失败可以被分解到一个名为 fail 的辅助函数中：

def fail (err : ε) : Except ε α := Except.error err

使用 ok 和 fail 会使 get 稍微更易读：

def get (xs : List α) (i : Nat) : Except String α := match xs[i]? with | none => fail s!"Index {i} not found (maximum is {xs.length - 1})" | some x => ok x

添加 andThen 的中缀声明后，firstThird 可以像返回 Option 的版本一样简洁：

infixl:55 " ~~> " => andThendef firstThird (xs : List α) : Except String (α × α) := get xs 0 ~~> fun first => get xs 2 ~~> fun third => ok (first, third)

这种技术同样可以扩展到更大的函数：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) := get xs 0 ~~> fun first => get xs 2 ~~> fun third => get xs 4 ~~> fun fifth => get xs 6 ~~> fun seventh => ok (first, third, fifth, seventh)

如果一个数除以 2 后没有余数，则它是偶数：

def isEven (i : Int) : Bool := i % 2 == 0

函数 sumAndFindEvens 在计算列表之和的同时，记住过程中遇到的偶数：

def sumAndFindEvens : List Int → List Int × Int | [] => ([], 0) | i :: is => let (moreEven, sum) := sumAndFindEvens is (if isEven i then i :: moreEven else moreEven, sum + i)

此函数是一个常见模式的简化示例。 许多程序需要遍历一次数据结构，同时既计算一个主要结果，又累积某种第三类附加结果。 日志记录就是一个例子：作为 IO 动作的程序总是可以记录到磁盘上的文件中，但由于磁盘处于 Lean 函数的数学世界之外，基于 IO 证明关于日志的性质就会困难得多。 另一个例子是这样一个函数：它通过中序遍历计算一棵树中所有节点的和，同时记录访问过的每个节点：

def inorderSum : BinTree Int → List Int × Int | BinTree.leaf => ([], 0) | BinTree.branch l x r => let (leftVisited, leftSum) := inorderSum l let (hereVisited, hereSum) := ([x], x) let (rightVisited, rightSum) := inorderSum r (leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)

BinTree.branch
  (BinTree.branch
    (BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
    (2, "c")
    (BinTree.leaf))
  (3, "d")
  (BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))

树最自然地用递归函数处理，但通常的树递归模式使得计算中序编号变得困难。 这是因为左子树中任意位置所分配的最大编号既用于确定某个节点数据值的编号，又再次用于确定右子树编号的起点。 在命令式语言中，可以通过使用一个包含下一个待分配编号的可变变量来绕过这个问题。 下面的 Python 程序使用可变变量计算中序编号：

class Branch:
    def __init__(self, value, left=None, right=None):
        self.left = left
        self.value = value
        self.right = right
    def __repr__(self):
        return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'

def number(tree):
    num = 0
    def helper(t):
        nonlocal num
        if t is None:
            return None
        else:
            new_left = helper(t.left)
            new_value = (num, t.value)
            num += 1
            new_right = helper(t.right)
            return Branch(left=new_left, value=new_value, right=new_right)

    return helper(tree)

与 aTree 等价的 Python 程序的编号为：

a_tree = Branch("d",
                left=Branch("c",
                            left=Branch("a", left=None, right=Branch("b")),
                            right=None),
                right=Branch("e"))

而它的编号为：

Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))

正如 Python 示例使用一个外层函数来建立可变变量，并使用一个内层辅助函数来改变该变量一样，这个函数的 Lean 版本使用一个外层函数来提供该变量的起始值，并显式返回函数的结果；同时使用一个内层辅助函数，在计算已编号树的过程中穿引该变量的值：

def number (t : BinTree α) : BinTree (Nat × α) := let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α)) | BinTree.leaf => (n, BinTree.leaf) | BinTree.branch left x right => let (k, numberedLeft) := helper n left let (i, numberedRight) := helper (k + 1) right (i, BinTree.branch numberedLeft (k, x) numberedRight) (helper 0 t).snd

这段代码与传播 none 的 Option 代码、传播 error 的 Except 代码以及累积日志的 WithLog 代码一样，混合了两个关注点：传播计数器的值，以及实际遍历树来寻找结果。 正如在那些情形中一样，可以定义一个 andThen 辅助函数，将状态从计算的一步传播到下一步。 第一步是为这样一种模式命名：以输入状态作为参数，并返回输出状态以及一个值：

def State (σ : Type) (α : Type) : Type := σ → (σ × α)

在 State 的情况下，ok 是一个函数，它返回未改变的输入状态，并同时返回给定的值：

def ok (x : α) : State σ α := fun s => (s, x)

处理可变变量时，有两个基本操作：读取其值，以及用一个新值替换它。 读取当前值是通过一个函数完成的，该函数将输入状态不加修改地放入输出状态，同时也将其放入值字段：

def get : State σ σ := fun s => (s, s)

写入一个新值包括忽略输入状态，并将所提供的新值放入输出状态中：

def set (s : σ) : State σ Unit := fun _ => (s, ())

最后，可以将两个使用状态的计算按顺序组合：先求出第一个函数的输出状态和返回值，然后将二者都传入下一个函数：

def andThen (first : State σ α) (next : α → State σ β) : State σ β := fun s => let (s', x) := first s next x s' infixl:55 " ~~> " => andThen

使用 State 及其辅助函数，可以模拟局部可变状态：

def number (t : BinTree α) : BinTree (Nat × α) := let rec helper : BinTree α → State Nat (BinTree (Nat × α)) | BinTree.leaf => ok BinTree.leaf | BinTree.branch left x right => helper left ~~> fun numberedLeft => get ~~> fun n => set (n + 1) ~~> fun () => helper right ~~> fun numberedRight => ok (BinTree.branch numberedLeft (n, x) numberedRight) (helper t 0).snd

因为 State 只模拟一个局部变量，所以 get 和 set 不需要引用任何特定的变量名。