Nat

Nat 是 Lean 及许多依赖类型编程语言中表示自然数（非负整数）的内置类型，是形式化数学与程序验证中最常用的基础类型之一，支持归纳定义与递归计算。