标签: kind-lang

在 Kind-Lang 等函数式语言助手中，自然数通常被形式化为具有两个构造函数（零和 succ）的递归代数数据类型：

type Nat {
  zero
  succ(pred: Nat)
}

至于 Int 类型，它也包含负数，在 Kind 上对其进行编码的最佳方法是什么？