From 653188ecd54c01af259d259dcb077deb25a75e08 Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Sat, 11 Oct 2025 01:57:34 +0800 Subject: [PATCH] update url --- docs/index.md | 12 ++++++------ docs/projects/meta-example.md | 4 ++-- docs/tutorial/elan-lake.md | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/docs/index.md b/docs/index.md index cf37876..cbc33b6 100644 --- a/docs/index.md +++ b/docs/index.md @@ -15,7 +15,7 @@ description: Lean-zh Documentation Telegram Badge - + Website @@ -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/) **进行中** diff --git a/docs/projects/meta-example.md b/docs/projects/meta-example.md index d723743..08be169 100644 --- a/docs/projects/meta-example.md +++ b/docs/projects/meta-example.md @@ -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) **准备工作** @@ -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)。 ### 交互式程序 diff --git a/docs/tutorial/elan-lake.md b/docs/tutorial/elan-lake.md index 51faf5c..9fde8dd 100644 --- a/docs/tutorial/elan-lake.md +++ b/docs/tutorial/elan-lake.md @@ -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` 替换为你自己起的名字）