Lean 策略编程指南（中文）

这是 lean-tactic-programming-guide 的中文 Verso 版。原有三个英文 .lean 教程完整保留，中文正文位于 Book/，可运行代码随书构建。

本地构建

需要与 lean-toolchain 一致的 Lean/ Lake（当前为 v4.30.0-rc2）。

lake update
lake build
lake exe examples
lake exe book --output _site

多页 HTML 位于 _site/html-multi/。因代码悬浮提示需要 HTTP，请用静态服务器预览：

python3 -m http.server 8000 --directory _site/html-multi

目录约定

• Book.lean：Verso Manual 根文档；
• Book/*.lean：中文章节；
• BookMain.lean：book 可执行文件和渲染配置；
• TacticProgrammingGuide.lean、CustomRw.lean、CustomSimp.lean：保留的上游教程源文件（含故意失败的教学片段与练习）；
• Book/Support/*.lean：受 Verso 内嵌环境限制的代码所用的编译支持模块；
• Examples.lean：最小的整体编译、运行示例入口；
• STANDARDS.md、GLOSSARY.md：写作规范与术语表；
• UPSTREAM.md、PROGRESS.md：上游同步与迁移进度。

贡献

开始翻译前请阅读上述四个维护文件。尤其要注意：所有可能被 Verso 拆成独立页面的 part 都必须显式设置稳定的 ASCII file 元数据，不能依赖中文标题自动生成 slug。