使用 类型与类型判断 的七条类型规则， 良类型与不良类型的含义见 良类型 ．

先看良类型的例子． 要说明 $\text{if }\left(\text{iszero }0\right)\text{ then }\text{ succ }0\text{ else }0:\text{ Nat}$，可以从结论往上搭推导． 项的最外层是 $\text{if}$，结论形如 $\text{if }\dots :𝑇$ 的规则只有 T-If； 取 $𝑇=\text{ Nat}$，它要求 $\text{iszero }0:\text{ Bool}$、$\text{succ }0:\text{ Nat}$、$0:\text{ Nat}$ 三个前提． 第一个前提 $\text{iszero }0:\text{ Bool}$ 只能匹配 T-IsZero（结论类型恰好是 $\text{Bool}$），再由 T-Zero 满足其前提 $0:\text{ Nat}$； 第二个前提 $\text{succ }0:\text{ Nat}$ 用 T-Succ，再接 T-Zero； 第三个前提 $0:\text{ Nat}$ 直接用 T-Zero． 每个前提都搭上了，合起来就是完整的推导：

再看不良类型的例子． 要说明 $\text{succ }\text{ true}$ 没有类型， 得证明对任何 $𝑇$ 都搭不出 $\text{succ }\text{ true }:𝑇$ 的推导． 逐一检查七条规则：结论左边形如 $\text{succ }\dots$ 的规则只有 T-Succ，其余六条形状不符，直接排除； 若存在推导，最后一步只能是 T-Succ，此时 $𝑇=\text{ Nat}$，且前提要求 $\text{true }:\text{ Nat}$． 再看 $\text{true }:\text{ Nat}$，结论左边为 $\text{true}$ 的规则只有 T-True，但 T-True 给出的类型是 $\text{Bool}$，与所需的 $\text{Nat}$ 冲突，没有别的规则可选． 唯一可能作为最后一步的 T-Succ 无法满足前提， 因此不存在合法的推导树，$\text{succ }\text{ true}$ 是不良类型的．