From 5f6bb8aace49cd414770d3ba28cc202c00f66fde Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Thu, 9 Jan 2025 13:16:28 +0800 Subject: [PATCH] reorganize files --- docs/index.md | 3 ++- docs/projects/blueprints.md | 3 +++ docs/{tutorial => projects}/jixia.md | 0 docs/{tutorial => projects}/lean4game.md | 0 docs/{tutorial => projects}/lean4web.md | 0 mkdocs.yml | 7 ++++--- 6 files changed, 9 insertions(+), 4 deletions(-) create mode 100644 docs/projects/blueprints.md rename docs/{tutorial => projects}/jixia.md (100%) rename docs/{tutorial => projects}/lean4game.md (100%) rename docs/{tutorial => projects}/lean4web.md (100%) diff --git a/docs/index.md b/docs/index.md index 4712331..6d8a3e5 100644 --- a/docs/index.md +++ b/docs/index.md @@ -59,7 +59,8 @@ Lean-zh 提供了一个学习与实践的平台,如果你对 Lean 感兴趣, **进行中** * [Lean 形式化数学(Mathematics in Lean)](https://www.leanprover.cn/math-in-lean-zh/) -* Lean 交互工具和实用项目的教程介绍 +* Lean 交互工具的使用教程 +* Lean 项目的实践教程 **计划进行** diff --git a/docs/projects/blueprints.md b/docs/projects/blueprints.md new file mode 100644 index 0000000..1eb9678 --- /dev/null +++ b/docs/projects/blueprints.md @@ -0,0 +1,3 @@ +# Lean Bleu Print + +项目地址:https://github.com/PatrickMassot/leanblueprint \ No newline at end of file diff --git a/docs/tutorial/jixia.md b/docs/projects/jixia.md similarity index 100% rename from docs/tutorial/jixia.md rename to docs/projects/jixia.md diff --git a/docs/tutorial/lean4game.md b/docs/projects/lean4game.md similarity index 100% rename from docs/tutorial/lean4game.md rename to docs/projects/lean4game.md diff --git a/docs/tutorial/lean4web.md b/docs/projects/lean4web.md similarity index 100% rename from docs/tutorial/lean4web.md rename to docs/projects/lean4web.md diff --git a/mkdocs.yml b/mkdocs.yml index 7de8f02..2509afd 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -78,9 +78,10 @@ nav: - PantoGraph 教程: tutorial/pantograph.md - Lean4 Jupyter: tutorial/lean4-jupyter.md - 项目教程: - - Lean4web 在线编译器: tutorial/lean4web.md - - jixia 数据分析: tutorial/jixia.md - - Lean4Game 教程: tutorial/lean4game.md + - Lean4web 在线编译器: projects/lean4web.md + - jixia 数据分析: projects/jixia.md + - Lean4Game 教程: projects/lean4game.md + - BleuPrints 教程: projects/bleuprints.md - 贡献指南: - 文档翻译: contribute/translation.md - 项目教程: contribute/project.md \ No newline at end of file