From 1c110919a63f3236d0d596ab56e3dc315e779fc4 Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Sun, 23 Jun 2024 04:25:45 +0800 Subject: [PATCH] fix bold space --- interacting_with_lean.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interacting_with_lean.md b/interacting_with_lean.md index 14aa503..94ac9e2 100644 --- a/interacting_with_lean.md +++ b/interacting_with_lean.md @@ -74,7 +74,7 @@ Importing is transitive. In other words, if you import ``Foo`` and ``Foo`` impor then you also have access to the contents of ``Bar``, and do not need to import it explicitly. --> -导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 +导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于 Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 导入是传递性的。换句话说，如果你导入了 ``Foo``，并且 ``Foo`` 导入了 ``Bar``，那么你也可以访问 ``Bar`` 的内容，而不需要明确导入它。