Nat

Nat is the built-in type representing natural numbers (non-negative integers) in Lean and many dependently typed programming languages. It is one of the most commonly used fundamental types in formal mathematics and program verification, supporting inductive definition and recursive computation.