Glimpse Of Lean

发表于 更新于 分类于 阅读次数： 字数： 219 时间 ≈ 1 分钟

唠唠闲话

安装配置

如果不方便配置环境，或者只是想快速了解这门语言，推荐使用在线服务，gitpod 或者 github-codespaces。

下边介绍本地运行方式，LEAN4 的安装可参考教程：「Lean 4 安装教程」。

此外，安装依赖的过程，需要下载 GitHub 资源，确保网络畅通。

下载仓库：

1
git clone https://github.com/Lean-zh/GlimpseOfLean.git

首次打开，需等待构建，如下图：

20240604153815

当然，也可以选择在命令行进行构建，使用 lake 包管理命令。

1
2
lake update # 更新依赖包
lake build # 构建依赖

构建阶段要编译 mathlib 库，通常要等待较长时间。

快速示例

我们仅介绍 GlimpseOfLean 的引用的例子。其他内容可以翻阅翻译的文档。此外，只有看是不够的，建议上手练习，一共就几个文件。