当递减参数是函数的具名形参时，可以直接引用其名称来指定。

def half (n : Nat) : Nat := match n with | 0 | 1 => 0 | n + 2 => half n + 1 termination_by structural n

当递减参数在签名中未命名时，可以在 Lean.Parser.Command.declaration : commandtermination_by 子句中局部引入一个名称。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1 termination_by structural n => n

递减参数的类型必须是归纳类型。 在 notInductive 中，被指定为递减参数的是一个函数：

def notInductive (x : Nat → Nat) : Nat := notInductive (fun n => x (n+1)) cannot use specified measure for structural recursion: its type is not an inductivetermination_by structural x

cannot use specified measure for structural recursion:
  its type is not an inductive

若递减参数是索引族，则所有索引都必须是变量。 在 constantIndex 中，索引族 Fin' 却被应用到了一个常量值上：

inductive Fin' : Nat → Type where | zero : Fin' (n+1) | succ : Fin' n → Fin' (n+1) def constantIndex (x : Fin' 100) : Nat := constantIndex .zero cannot use specified measure for structural recursion: its type Fin' is an inductive family and indices are not variables Fin' 100termination_by structural x

cannot use specified measure for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

递减参数类型中的参数，不能依赖那些位于变化参数或索引之后的函数形参。 在 afterVarying 中，固定前缀 为空，因为第一个形参 n 会变化，所以 p 不属于固定前缀：

inductive WithParam' (p : Nat) : Nat → Type where | zero : WithParam' p (n+1) | succ : WithParam' p n → WithParam' p (n+1) failed to infer structural recursion: Cannot use parameter x: failed to eliminate recursive application afterVarying (n + 1) p WithParam'.zero def afterVarying (n : Nat) (p : Nat) (x : WithParam' p n) : Nat := afterVarying (n+1) p .zero termination_by structural x

failed to infer structural recursion:
Cannot use parameter x:
  failed to eliminate recursive application
    afterVarying (n + 1) p WithParam'.zero

在下例中，递减参数 n 与嵌套模式 .succ (.succ n) 匹配。因此 .succ (.succ n) 是 n 的一个（非严格）子项，于是 n 和 .succ n 都是真子项，所以该定义会被接受。

def fib : Nat → Nat | 0 | 1 => 1 | .succ (.succ n) => fib n + fib (.succ n) termination_by structural n => n

为便于说明，这个例子使用 .succ n 和 .succ (.succ n)，而不是等价的、Nat 专用的 n+1 与 n+2。

在下例中，递减参数 n 并不是 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 表达式的直接 判别项。 因此，n' 不会被视为 n 的子项。

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application half n' def half (n : Nat) : Nat := match Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    half n'

若改用 良基递归，并显式把判别项与匹配模式联系起来，这个定义就能被接受。

def half (n : Nat) : Nat := match h : Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by n decreasing_by simp_alln:Natn':Nath:n = n' + 1 + 1⊢ n' < n' + 1 + 1; omegaAll goals completed! 🐙

类似地，下面这个例子也会失败：虽然 xs.tail 会归约为 xs 的一个真子项，但按照上述规则，这一点对 Lean 来说并不可见。 特别地，xs.tail 与 xs 的某个真子项并不 定义相等。

failed to infer structural recursion: Cannot use parameter #2: failed to eliminate recursive application listLen xs.tail def listLen : List α → Nat | [] => 0 | xs => listLen xs.tail + 1 termination_by structural xs => xs

用于证明终止性的这些策略有一个重要后果：同时匹配两个 判别项 与匹配一个二元组并不等价。 同时匹配会保留判别项与模式之间的联系，使模式匹配不仅能细化局部上下文中假设的类型，也能细化 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 的期望类型。 本质上，Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 的精译规则会对判别项作特殊处理；因此，对判别项做出虽能保持程序运行时含义、却不一定保持编译时含义的改动，并不安全。

下面这个求两个自然数最小值的函数，是按其第一个参数做结构递归定义的：

def min' (n k : Nat) : Nat := match n, k with | 0, _ => 0 | _, 0 => 0 | n' + 1, k' + 1 => min' n' k' + 1 termination_by structural n

若把对两个参数的同时模式匹配改写为对一个二元组做匹配，终止性分析就会失败：

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application min' n' k' def min' (n k : Nat) : Nat := match (n, k) with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' n' k' + 1 termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    min' n' k'

这是因为在把递归调用与更小的实参值对应起来时，该分析只考虑对形参本身的直接模式匹配。 把判别项包进一个二元组会破坏这种联系。

下面这个求一对数中两个分量之最小值的函数，无法通过结构递归精译。

failed to infer structural recursion: Cannot use parameter nk: the type Nat × Nat does not have a `.brecOn` recursor def min' (nk : Nat × Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by structural nk

failed to infer structural recursion:
Cannot use parameter nk:
  the type Nat × Nat does not have a `.brecOn` recursor

这是因为该形参的类型 Prod 并不是递归的。 因此，它的构造器没有可通过模式匹配暴露出来的递归参数。

不过，这个定义可以通过 良基递归 被接受：

def min' (nk : Nat × Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by nk

尽管 countdown 的递归出现被应用到了一个并非递减参数真子项的项上，下列定义仍会被接受：

def countdown (n : Nat) : List Nat := match n with | 0 => [] | n' + 1 => n' :: countdown (n' + 0) termination_by structural n

这是因为 n' + 0 与 n' 定义相等，而后者是 n 的真子项。 由模式匹配产生的 子项 会通过 匹配泛化 的规则与 判别项 关联起来，而这些规则尊重定义相等。

在 countdown' 中，递归出现被应用到了 0 + n' 上；它与 n' 并不定义相等，因为自然数上的加法是按照第二个参数做结构递归的：

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application countdown' (0 + n') def countdown' (n : Nat) : List Nat := match n with | 0 => [] | n' + 1 => n' :: countdown' (0 + n') termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    countdown' (0 + n')

下面这个例子展示了在一个非互递归的归纳数据类型上进行互递归：

mutual def even : Nat → Prop | 0 => True | n+1 => odd n termination_by structural n => n def odd : Nat → Prop | 0 => False | n+1 => even n termination_by structural n => n end

下面这个例子展示了在互归纳类型上的递归。 函数 Exp.size 与 App.size 互相递归。

mutual inductive Exp where | var : String → Exp | app : App → Exp inductive App where | fn : String → App | app : App → Exp → App end mutual def Exp.size : Exp → Nat | .var _ => 1 | .app a => a.size termination_by structural e => e def App.size : App → Nat | .fn _ => 1 | .app a e => a.size + e.size + 1 termination_by structural a => a end

App.numArgs 的定义是在类型 App 上做结构递归。 它说明互递归组中的归纳类型不必全部都参与处理。

def App.numArgs : App → Nat | .fn _ => 0 | .app a _ => a.numArgs + 1 termination_by structural a => a

Lean 会自动推断函数 half 是结构递归的。 termination_by? 子句会显示推断出的终止性注解，并且可以一键自动加入源文件。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1 Try this: [apply] termination_by structural x => xtermination_by?

Try this:
  [apply] termination_by structural x => x

自然数加法可通过对第二个参数递归来定义。 这个函数显然是结构递归的。

def add (n : Nat) : Nat → Nat | .zero => n | .succ k => .succ (add n k)

若使用 Nat.rec 定义，它就会远离大多数人习惯的记法。

def add' (n : Nat) := Nat.rec (motive := fun _ => Nat) n (fun Variable name `k` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _k Note: This linter can be disabled with `set_option linter.unusedVariables false`k soFar => .succ soFar)

若结构递归调用所用的数据并非函数参数的直接子项，就需要发挥创意，或采用复杂但系统的编码。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1

理解这个函数的一种方式，是将它看作一种结构递归：每次调用都翻转一个位，并且仅在该位已设置时递增结果。

def helper : Nat → Bool → Nat := Nat.rec (motive := fun _ => Bool → Nat) (fun _ => 0) (fun _ soFar => fun b => (if b then Nat.succ else id) (soFar !b)) def half' (n : Nat) : Nat := helper n false [0, 0, 1, 1, 2, 2, 3, 3, 4]#eval [0, 1, 2, 3, 4, 5, 6, 7, 8].map half'

[0, 0, 1, 1, 2, 2, 3, 3, 4]

无需发挥创意，可以改用一种称为所有较小值递归的通用技术。 所有较小值递归使用可针对每个归纳类型系统推导出的辅助定义；这些辅助定义以递归器来定义，Lean 会自动推导它们。 对于每个 Nat 值 n，类型 n.below (motive := mot) 为所有 k < n 提供一个类型为 mot k 的值，并将其表示为迭代的 依赖序对类型。 所有较小值递归器 Nat.brecOn 允许函数使用任意更小 Nat 值所对应的结果。 用它定义函数并不方便：

noncomputable def half'' (n : Nat) : Nat := Nat.brecOn n (motive := fun _ => Nat) fun k soFar => match k, soFar with | 0, _ | 1, _ => 0 | _ + 2, ⟨_, ⟨h, _⟩⟩ => h + 1

该函数被标记为 Lean.Parser.Command.declaration : commandnoncomputable，因为编译器不支持为所有较小值递归生成代码；这种递归旨在用于推理，而非生成高效代码。 不过，仍然可以使用内核测试该函数：

[0, 0, 1, 1, 2, 2, 3, 3, 4]#reduce [0,1,2,3,4,5,6,7,8].map half''

[0, 0, 1, 1, 2, 2, 3, 3, 4]

如有必要，half'' 函数体中的依赖模式匹配也可使用递归器（具体来说是 Nat.casesOn）来编码：

noncomputable def half''' (n : Nat) : Nat := n.brecOn (motive := fun _ => Nat) fun k => k.casesOn (motive := fun k' => (k'.below (motive := fun _ => Nat)) → Nat) (fun _ => 0) (fun k' => k'.casesOn (motive := fun k'' => (k''.succ.below (motive := fun _ => Nat)) → Nat) (fun _ => 0) (fun _ soFar => soFar.2.1.succ))

这个定义仍然有效。

[0, 0, 1, 1, 2, 2, 3, 3, 4]#reduce [0,1,2,3,4,5,6,7,8].map half''

[0, 0, 1, 1, 2, 2, 3, 3, 4]

然而，它现在已远离原始定义，而且变得难以为大多数人所理解。 递归器是出色的逻辑基础，却不是编写程序或证明的简便方式。

此定义等价于 List.below：

def List.below' {α : Type u} {motive : List α → Sort u} : List α → Sort (max (u + 1) u) | [] => PUnit | _ :: xs => motive xs ×' xs.below' (motive := motive)

换言之，对于给定的动机，List.below' 是一个包含该动机在列表所有后缀上的实现的类型。

递归参数越多，就需要对积类型进行更深层的嵌套迭代。 例如，二叉树有两个递归出现。

inductive Tree (α : Type u) : Type u where | leaf | branch (left : Tree α) (val : α) (right : Tree α)

其对应的所有较小值递归表包含该动机在所有子树上的实现：

def Tree.below' {α : Type u} {motive : Tree α → Sort u} : Tree α → Sort (max (u + 1) u) | .leaf => PUnit | .branch left _val right => (motive left ×' left.below' (motive := motive)) ×' (motive right ×' right.below' (motive := motive))

对于列表和树，brecOn 运算符都只要求一个分支，而不是每个构造器各有一个分支。 该分支接收一个列表或树，以及所有较小值的结果表；它应据此满足所给值的动机。 对所给值进行依赖分情况分析会自动精化记忆表的类型，从而提供所需的一切。

以下定义分别等价于 List.brecOn 和 Tree.brecOn。 原始递归辅助函数 List.brecOnTable 和 Tree.brecOnTable 在计算最终结果的同时计算所有较小值递归表，而 brecOn 运算符的实际定义只是投影出结果。

def List.brecOnTable {α : Type u} {motive : List α → Sort u} (xs : List α) (step : (ys : List α) → ys.below' (motive := motive) → motive ys) : motive xs ×' xs.below' (motive := motive) := match xs with | [] => ⟨step [] PUnit.unit, PUnit.unit⟩ | x :: xs => let res := xs.brecOnTable (motive := motive) step let val := step (x :: xs) res ⟨val, res⟩ def Tree.brecOnTable {α : Type u} {motive : Tree α → Sort u} (t : Tree α) (step : (ys : Tree α) → ys.below' (motive := motive) → motive ys) : motive t ×' t.below' (motive := motive) := match t with | .leaf => ⟨step .leaf PUnit.unit, PUnit.unit⟩ | .branch left val right => let resLeft := left.brecOnTable (motive := motive) step let resRight := right.brecOnTable (motive := motive) step let branchRes := ⟨resLeft, resRight⟩ let val := step (.branch left val right) branchRes ⟨val, branchRes⟩ def List.brecOn' {α : Type u} {motive : List α → Sort u} (xs : List α) (step : (ys : List α) → ys.below' (motive := motive) → motive ys) : motive xs := (xs.brecOnTable (motive := motive) step).1 def Tree.brecOn' {α : Type u} {motive : Tree α → Sort u} (t : Tree α) (step : (ys : Tree α) → ys.below' (motive := motive) → motive ys) : motive t := (t.brecOnTable (motive := motive) step).1

逐步考察 half 的精译时，第一步是手工把它反糖化成一个更简单的形式。 这并不完全符合 Lean 的实际处理方式，但当出现的 OfNat 实例更少时，输出会容易阅读得多。 这个较易读的定义：

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1

可以改写成下面这个更底层一些的版本：

def half : Nat → Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

精译器一开始会先精译出一个预定义，其中递归仍然保留，但除此之外，该定义已经落在 Lean 的核心类型论里。 开启编译器对预定义的追踪，并让美化打印更显式，就可以看到得到的预定义：

set_option trace.Elab.definition.body true in set_option pp.all true in [Elab.definition.body] half : Nat → Nat := fun (x : Nat) => half.match_1.{1} (fun (x : Nat) => Nat) x (fun (_ : Unit) => Nat.zero) (fun (_ : Unit) => Nat.zero) fun (n : Nat) => Nat.succ (half n)def half : Nat → Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

返回的跟踪消息是：

[Elab.definition.body] half : Nat → Nat :=
    fun (x : Nat) =>
      half.match_1.{1} (fun (x : Nat) => Nat) x
        (fun (_ : Unit) => Nat.zero)
        (fun (_ : Unit) => Nat.zero)
        fun (n : Nat) => Nat.succ (half n)

辅助匹配函数的定义是：

@[instance_reducible] def half.match_1.{u_1} : (motive : Nat → Sort u_1) → (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x := fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n#print half.match_1

@[instance_reducible] def half.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x :=
fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

把它排版得更易读一些，则为：

def half.match_1'.{u} : (motive : Nat → Sort u) → (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x := fun Variable name `motive` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _motive Note: This linter can be disabled with `set_option linter.unusedVariables false`motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

换言之，half 中使用的那组特定模式配置，被编码进了 half.match_1。

这个定义是 half 预定义的一个更易读版本：

def half' : Nat → Nat := fun (x : Nat) => half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- 0 的分支 (fun _ => 0) -- 1 的分支 (fun n => Nat.succ (half' n)) -- n + 2 的分支

要把它精译为一个结构递归函数，第一步是建立对 bRecOn 的调用。 该定义必须标记为 Lean.Parser.Command.declaration : commandnoncomputable，因为 Lean 不支持为 Nat.brecOn 这类递归器生成代码。

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => don't know how to synthesize placeholder context: x n:Nattable:Nat.below n⊢ Nat_ /- 待翻译： half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- 0 的分支 (fun _ => 0) -- 1 的分支 (fun n => Nat.succ (half' n)) -- n + 2 的分支 -/

下一步是把原函数体中出现的 x 替换为 brecOn 提供的 n。 由于 table 的类型依赖于 x，因此在用 half.match_1 分情况时，它也必须一并泛化，从而得到一个带额外参数的动机。

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n don't know how to synthesize placeholder for argument `h_1` context: x n:Nattable:Nat.below n⊢ Unit → Nat.below Nat.zero → Nat_ don't know how to synthesize placeholder for argument `h_2` context: x n:Nattable:Nat.below n⊢ Unit → Nat.below 1 → Nat_ don't know how to synthesize placeholder for argument `h_3` context: x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat_) table /- 待翻译： (fun _ => 0) -- 0 的分支 (fun _ => 0) -- 1 的分支 (fun n => Nat.succ (half' n)) -- n + 2 的分支 -/

这三个分支中的占位符分别需要如下类型：

don't know how to synthesize placeholder for argument `h_1`
context:
x n:Nattable:Nat.below n⊢ Unit → Nat.below Nat.zero → Nat

don't know how to synthesize placeholder for argument `h_2`
context:
x n:Nattable:Nat.below n⊢ Unit → Nat.below 1 → Nat

don't know how to synthesize placeholder for argument `h_3`
context:
x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat

预定义中的前两个分支都是常量函数，没有递归需要检查：

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n (fun () _ => .zero) (fun () _ => .zero) don't know how to synthesize placeholder for argument `h_3` context: x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat_) table /- 待翻译： (fun n => Nat.succ (half' n)) -- n + 2 的分支 -/

最后一个分支包含递归调用。 它应当被翻译为对“所有较小值表”的一次查找。 最后一个洞的类型，用更易读的形式写出来是：

(n : Nat) → Nat.below (motive := fun _ => Nat) n.succ.succ → Nat

它等价于

(n : Nat) → Nat ×' (Nat ×' Nat.below (motive := fun _ => Nat) n) → Nat

“所有较小值表”中的第一个 Nat，是对 n + 1 递归所得的结果；第二个则是对 n 递归所得的结果。 因此，递归调用可以替换成一次查找，于是精译成功：

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n (fun () _ => .zero) (fun () _ => .zero) (fun _ table => Nat.succ table.2.1) table unexpected end of input; expected ')', ',' or ':'

实际的精译器会在动机中插入带新鲜名称的哨兵类型，以此跟踪“当前检查是否结构递归的参数”与“所有较小值表中的位置”之间的对应关系。

函数类型一般并没有对终止性证明有用的良基关系。 因此，实例合成会选中 instSizeOfDefault 及其对应的良基关系。 如果度量本身是一个函数，那么就会选中默认的 SizeOf 实例，证明也就不可能成功。

declaration uses `sorry`def declaration uses `sorry`fooInst (b : Bool → Bool) : Unit := fooInst (b ∘ b) termination_by b decreasing_by guard_target = @sizeOf (Bool → Bool) (instSizeOfDefault _) (b ∘ b) < sizeOf bb:Bool → Bool⊢ sizeOf (b ∘ b) < sizeOf b simp only [sizeOf, default.sizeOf]b:Bool → Bool⊢ 0 < 0 guard_target = 0 < 0b:Bool → Bool⊢ 0 < 0 simpb:Bool → Bool⊢ False guard_target = Falseb:Bool → Bool⊢ False sorryAll goals completed! 🐙

下面这个 Fibonacci 数的递归定义有两个递归调用，因此终止性证明中会产生两个目标。

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n unsolved goals n:Nath:¬n ≤ 1⊢ n - 1 < n n:Nath:¬n ≤ 1⊢ n - 2 < ndecreasing_by skipn:Nath:¬n ≤ 1⊢ n - 1 < nn:Nath:¬n ≤ 1⊢ n - 2 < n

这里的 度量 就是参数本身，而良基顺序则是自然数上的小于关系。 第一个证明目标要求用户证明：第一次递归调用的实参，也就是 n - 1，严格小于函数的形参 n。

这两个终止性证明都可以很容易地用 omega 策略解决。

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n decreasing_by ·n:Nath:¬n ≤ 1⊢ n - 1 < n omegaAll goals completed! 🐙 ·n:Nath:¬n ≤ 1⊢ n - 2 < n omegaAll goals completed! 🐙