它简单地指定了零为偶数，一为奇数，然后递归地说明了 k+2 的奇偶性与 k 相同。 显式地标出 n 是奇 数还是偶数对于类型推断来说是必须的。然而，类型检查器却拒绝了它： viewsbroken.idr:12:10: 在解析 ViewsBroken.parity 的右侧时： Parity (plus (S j) (S j)) 与 Parity (S (S (plus j j))) 的类型不匹配 具体为： plus (S • 非 非 非终 终 终止 止 止符 符 符（ （ （Non - t e r m i n al ） ） ） — 位于方括号内，此处为 [test]、[t] 和 [e]，它们表示任意表达 式。为避免解析歧义，这些表达式不能在顶层使用语法扩展 （也就是说你可以在括号中使用）。 • 名 名 名称 称 称 — 位于大括号内，它表示可在右侧被绑定的名字。 • 符 符 符号 号 号 — 位于引号内，例如 啥时候能自举啊？ 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 夽 这事不急，虽说从长远来看这主意不错。就目前来说，实现支持自举的库是一项很有价值的工作夬 比如 说参数解析器以及符合 奐 奏 奓 奉 奘 标准的库用于系统交互。 2. 9 I d r i s 有 有 有全 全 全域 域 域多 多 多态 态 态不 不 不? Type 是 是 是啥 啥 啥类 类 类型 型