Cross-Reference Redirection
Cross-Reference Redirection
Table of Contents
1.
环境与运行约定
2.
Lean 4 元编程模型
3.
Expr：Lean 4 的内部表示
4.
编写你的第一个 Tactic
5.
目标管理
6.
Type Class Synthesis
7.
simp——化简的瑞士军刀
8.
ring 和
ring_nf
：代数范式化
9.
omega：Presburger 算术决策过程
10.
linarith、nlinarith 与 polyrith
11.
norm_num
：数值计算框架
12.
aesop：可配置的启发式搜索
13.
grind：E-matching 与 Congruence Closure
14.
decide 与
native_decide
：有限计算判定
15.
positivity：符号非负性推理
16.
fun_prop
：函数性质的自动证明
17.
gcongr：广义合同性
18.
field_simp
：分式化简
19.
push
neg、contrapose、by
contra
20.
设计你自己的领域自动化
21.
反射证明模式
22.
性能工程
23.
对接外部工具
24.
从证明模式到自动化：方法论
25.
迈向分析自动化
26.
附录 A：Metaprogramming API 速查表