Lean 4 类型检查

本文档旨在帮助读者更好地理解 Lean 的内核，解释使用 Lean 所涉及的信任假设，并为希望为 Lean 内核语言编写自己的外部类型检查器的读者提供资源。