Deploying to gh-pages from @ 1c11091 🚀

interacting_with_lean.html

@@ -202,7 +202,7 @@ <h2 id="导入文件"><a class="header" href="#导入文件">导入文件</a></h
 Importing is transitive. In other words, if you import ``Foo`` and ``Foo`` imports ``Bar``,
 then you also have access to the contents of ``Bar``, and do not need to import it explicitly.
 -->
-<p>导入文件 <code>Bar/Baz/Blah.olean</code>，其中的描述是相对于Lean <strong>搜索路径</strong> 解释的。关于如何确定搜索路径的信息可以在<a href="https://lean-lang.org/documentation/">文档</a>中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。</p>
+<p>导入文件 <code>Bar/Baz/Blah.olean</code>，其中的描述是相对于 Lean <strong>搜索路径</strong> 解释的。关于如何确定搜索路径的信息可以在<a href="https://lean-lang.org/documentation/">文档</a>中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。</p>
 <p>导入是传递性的。换句话说，如果你导入了 <code>Foo</code>，并且 <code>Foo</code> 导入了 <code>Bar</code>，那么你也可以访问 <code>Bar</code> 的内容，而不需要明确导入它。</p>
 <!--
 More on Sections

print.html

@@ -5600,7 +5600,7 @@ <h2 id="导入文件"><a class="header" href="#导入文件">导入文件</a></h
 Importing is transitive. In other words, if you import ``Foo`` and ``Foo`` imports ``Bar``,
 then you also have access to the contents of ``Bar``, and do not need to import it explicitly.
 -->
-<p>导入文件 <code>Bar/Baz/Blah.olean</code>，其中的描述是相对于Lean <strong>搜索路径</strong> 解释的。关于如何确定搜索路径的信息可以在<a href="https://lean-lang.org/documentation/">文档</a>中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。</p>
+<p>导入文件 <code>Bar/Baz/Blah.olean</code>，其中的描述是相对于 Lean <strong>搜索路径</strong> 解释的。关于如何确定搜索路径的信息可以在<a href="https://lean-lang.org/documentation/">文档</a>中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。</p>
 <p>导入是传递性的。换句话说，如果你导入了 <code>Foo</code>，并且 <code>Foo</code> 导入了 <code>Bar</code>，那么你也可以访问 <code>Bar</code> 的内容，而不需要明确导入它。</p>
 <!--
 More on Sections