使用 [定义] 类型与类型判断 的七条类型规则，良类型与不良类型的含义见 [定义] 良类型 。

良类型的例子。要说明 $\text{if }\left(\text{iszero }0\right)\text{ then }\text{ succ }0\text{ else }0:\text{ Nat}$，从结论往上搭推导：

1. 项的最外层是 $\text{if}$，结论形如 $\text{if }\dots :𝑇$ 的规则只有 T-If。取 $𝑇=\text{ Nat}$，它要求三个前提：$\text{iszero }0:\text{ Bool}$、$\text{succ }0:\text{ Nat}$、$0:\text{ Nat}$。
2. 第一个前提 $\text{iszero }0:\text{ Bool}$：只有 T-IsZero 的结论形如 $\text{iszero }\dots$，结论类型恰好是 $\text{Bool}$，它要求 $0:\text{ Nat}$。T-Zero 给出这一点。
3. 第二个前提 $\text{succ }0:\text{ Nat}$：用 T-Succ，它要求 $0:\text{ Nat}$，再用 T-Zero。
4. 第三个前提 $0:\text{ Nat}$：直接用 T-Zero。

每个前提都搭上了，合起来就是一棵完整的推导：

不良类型的例子。要说明 $\text{succ }\text{ true}$ 没有类型，得证明对任何 $𝑇$ 都搭不出 $\text{succ }\text{ true }:𝑇$ 的推导。我们可以直接穷举七条规则：

1. 结论左边形如 $\text{succ }\dots$ 的规则只有 T-Succ，其余六条的结论形状对不上，直接排除。所以如果有推导，最后一步只能是 T-Succ，此时 $𝑇=\text{ Nat}$，前提是 $\text{true }:\text{ Nat}$。
2. 再看 $\text{true }:\text{ Nat}$。结论左边是 $\text{true}$ 的规则只有 T-True，而它的结论是 $\text{true }:\text{ Bool}$，类型是 $\text{Bool}$ 不是 $\text{Nat}$，搭不上。没有别的规则可选。

唯一可能作为最后一步的 T-Succ 无法满足它的前提，因此不存在合法的推导树，$\text{succ }\text{ true}$ 是不良类型的。