Lean 语言参考
Lean 语言参考
Table of Contents
1.
引言
2.
精化和编译
3.
与 Lean 交互
4.
Type 系统
5.
源文件和模块
6.
命名空间和部分
7.
定义
8.
公理
9.
属性
10.
Type 类别
11.
强制
12.
运行时代码
13.
条款
14.
策略样张
15.
简化者
16.
grind
策略
17.
mvcgen
策略
18.
函子、Monad 和
do
表示法
19.
基本建设
20.
基本类型
21.
IO
22.
迭代器
23.
符号和宏
24.
构建工具和分发
验证 Lean 证明
错误说明
发行说明
支持的平台
索引
13.
条款
13.1.
标识符
13.2.
功能类型
13.3.
功能
13.4.
功能应用
13.5.
数字文字
13.6.
结构和构造函数
13.7.
条件句
13.8.
模式匹配
13.9.
洞
13.10.
Type 归属
13.11.
引用和反引用
13.12.
do
-符号
13.13.
证明
13.11.
引用和反引用
Source Code
Report Issues
←
13.10. Type 归属
13.12. do-符号
→
13.11. 引用和反引用
🔗
报价条款在
报价部分
中进行了描述。
←
13.10. Type 归属
13.12. do-符号
→