add metaprogram example

Author: RexWzh

docs/install.md

@@ -34,7 +34,7 @@ wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/s
 
 ```bash
 # 如果网络不行就本地下载再上传
-curl -L https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
+curl -L https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
 tar xf elan.tar.gz
 ```
 

docs/tutorial/repl.md

@@ -267,7 +267,7 @@ echo '{ "cmd": "import Mathlib" }' | lake env /path/to/repl/.lake/build/bin/repl
 
 ## 更多示例
 
-最后，附上 REPL 测试代码提供的示例，为展示方便，我们将输出结果拼接到对应的输入行后边。
+最后，附上 REPL 提供的测试示例，以下内容由模型结合测试代码生成。
 
 ### 基础示例：检查变量定义
 

mkdocs.yml

@@ -71,7 +71,8 @@ nav:
     - Lean-zh: index.md
     - 安装指南: install.md
     - Lean4 工具链: tutorial/elan-lake.md
-    - Lake 包管理: references/lake-doc.md   
+    - Lake 包管理: references/lake-doc.md
+    - 项目示例 - 元编程: projects/meta-example.md
   - 交互工具:
     - LeanDojo 教程: tutorial/lean-dojo.md
     - REPL 教程: tutorial/repl.md