Lean4 的元编程

函数式编程基础

以 Lean 4 构造定理证明器为主线，介绍归纳类型与模式匹配、用值表示失败、I/O、可证明终止的递归，以及组织这些计算结构的 Monad 接口。

Lean 前端与元编程流程

追踪 Lean 源代码到内核可检查的 Expr：解析生成 Syntax，CommandElabM 更新环境，TermElabM 将项 elaboration 为 Expr，MetaM/CoreM 提供类型论服务，并以 TacticM 展示证明目标的 elaboration 状态。