Study note

Metaprogramming in Lean 4

View original Back to list

Properties

Type: Books
Status: 想读
Domain: Compilers / PL
Category: 类型系统、形式化与定理证明
Source: leanprover-community.github.io
Vault note: library/books/compilers/Metaprogramming-in-Lean-4-ff6bfb58e31916e2.md

从 Lean 表达式、`MetaM`、语法、宏和 elaboration 逐步进入 DSL 与自定义 tactic 开发，解释 Lean 编译流程以及元编程 API 如何操作 `Expr`、`Syntax` 和证明目标。

适合在掌握普通 Lean 证明并理解 Monad 之后阅读；多数章节带练习和完整解答，可用于学习阅读 Lean/Mathlib 内部代码与编写证明自动化。

Lean 社区；持续更新。

Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics) Books · 类型系统、形式化与定理证明
Certified Programming with Dependent Types Books · 类型系统、形式化与定理证明
Software Foundations Books · 类型系统、形式化与定理证明
Theorem Proving in Lean 4 Books · 类型系统、形式化与定理证明
Type Theory and Formal Proof : An Introduction Books · 类型系统、形式化与定理证明
Types and Programming Languages Books · 类型系统、形式化与定理证明

Loading comments...