20. 基本类型🔗

Lean 包含一些由编译器提供特殊支持的内置类型。其中有些类型（例如 Nat）在内核中还有特殊支持。其他类型本身虽然没有特殊的编译器支持，但出于性能原因，它们在很大程度上依赖于类型的内部表示。