Skip to content

Add docs url #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RexWzh merged 1 commit into from
Oct 10, 2025
Merged

Add docs url #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions docs/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ description: Lean-zh Documentation
<a href="https://t.me/Lean_zh_CN">
<img src="https://img.shields.io/badge/Telegram-加入讨论-blue?style=flat&logo=telegram&logoColor=white" alt="Telegram Badge">
</a>
<a href="https://www.leanprover.cn">
<a href="https://docs.leanprover.cn">
<img src="https://img.shields.io/badge/Website-访问主页-blue.svg?style=flat" alt="Website">
</a>
</div>
Expand Down Expand Up @@ -52,11 +52,11 @@ Lean-zh 提供一个实践，交流，和知识分享的平台。如果你对 Le

目前 Lean-zh 已翻译的资源：

- [Lean4 函数式编程（Functional Programming in Lean）](https://www.leanprover.cn/fp-lean-zh/)
- [Lean4 定理证明（Theorem Proving in Lean）](https://www.leanprover.cn/tp-lean-zh/)
- [Lean4 元编程（Metaprogramming in Lean）](https://www.leanprover.cn/mp-lean-zh/)
- [Lean 形式化数学（Mathematics in Lean）](https://www.leanprover.cn/math-in-lean-zh/)
- [Lean4 中的类型检查（Type Checking in Lean）](https://www.leanprover.cn/type-checking-in-lean-zh/)
- [Lean4 函数式编程（Functional Programming in Lean）](/fp-lean-zh/)
- [Lean4 定理证明（Theorem Proving in Lean）](/tp-lean-zh/)
- [Lean4 元编程（Metaprogramming in Lean）](/mp-lean-zh/)
- [Lean 形式化数学（Mathematics in Lean）](/math-in-lean-zh/)
- [Lean4 中的类型检查（Type Checking in Lean）](/type-checking-in-lean-zh/)

**进行中**

Expand Down
4 changes: 2 additions & 2 deletions docs/projects/meta-example.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
**参考资源**

- 元编程示例教程：[MetaExamples](https://github.com/siddhartha-gadgil/MetaExamples)
- Lean 中文文档：[函数式编程](https://www.leanprover.cn/fp-lean-zh/)，[Lake 文档](../references/lake-doc.md)以及 [Lean4 安装指南](../install.md)
- Lean 中文文档：[函数式编程](/fp-lean-zh/)，[Lake 文档](../references/lake-doc.md)以及 [Lean4 安装指南](../install.md)

**准备工作**

Expand Down Expand Up @@ -263,7 +263,7 @@ import Hello.Greet
> - 而是一个描述了 IO 操作的声明性表达
> - 可以将 IO 操作视为一个接收"整个世界"作为输入，并返回新的世界状态的纯函数
>
> 更多关于 Lean 函数式编程的讨论，可以参考 [Lean 函数式编程指南](https://www.leanprover.cn/fp-lean-zh/hello-world/running-a-program.html)。
> 更多关于 Lean 函数式编程的讨论，可以参考 [Lean 函数式编程指南](/fp-lean-zh/hello-world/running-a-program.html)。


### 交互式程序
Expand Down
2 changes: 1 addition & 1 deletion docs/tutorial/elan-lake.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ elan 配置记录可以在 `~/.elan/settings.toml` 查看。

[lake](https://github.com/leanprover/lake) 全称 Lean Make，是 Lean 4 的包管理器，用于创建 Lean 项目，构建 Lean 包和编译 Lean 可执行文件。

本节介绍 `lake` 的基本用法，[Lean 函数式编程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)也提供了创建 Lean 项目的例子，而更全面的参数介绍可参考 [lake 文档](../references/lake-doc.md)。
本节介绍 `lake` 的基本用法，[Lean 函数式编程](/fp-lean-zh/hello-world/starting-a-project.html)也提供了创建 Lean 项目的例子，而更全面的参数介绍可参考 [lake 文档](../references/lake-doc.md)。

在终端中运行（`your_project_name` 替换为你自己起的名字）

Expand Down