Lean 4 类型检查 这是一本关于 Lean 4 内核和实现外部类型检查器的书;它是用 mdBook 构建的。 原作者:Christopher A. Bailey 原文地址:https://ammkrn.github.io/type_checking_in_lean4/ 译者:subfish_zhou 译本地址:http://www.leanprover.cn/type-checking-in-lean-zh/ 贡献 欢迎提交PR