Lean 4(元)编程 Cookbook
Lean 4(元)编程 Cookbook
Table of Contents
什么是元编程?
使用信息视图
语法与宏
使用表达式
精译(elaboration):扩展语法
策略
维护状态
I/O 与进程
文件系统
数据结构
索引
如何编写配方
Cookbook 贡献者
如何编写配方
添加章节
文本格式
贡献者区块
添加章节
元数据与标签
←
如何编写配方
元数据与标签
→
添加章节
🔗
一级小节使用
#
,如下所示。每个章节应从明确的问题陈述和解决办法概览开始,本节的写法就是一个例子。
内容内部可以用
##
组织二级小节。用
*
标记强调文字,例如
这样
。
元数据与标签
←
如何编写配方
元数据与标签
→