Merge pull request #14 from Lean-zh/add-docs-url

Add docs url

Author: RexWzh

docs/index.md

@@ -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>
@@ -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/)
 
 **进行中**
 

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)。
 
 
 ### 交互式程序

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` 替换为你自己起的名字）