Deploying to gh-pages from @ 8cb1712 🚀

dependent_type_theory.html

@@ -453,7 +453,7 @@ <h2 id="类型作为对象"><a class="header" href="#类型作为对象">类型
 that there is a ``Type n`` for every natural number ``n``. ``Type`` is
 an abbreviation for ``Type 0``:
 -->
-<p>可以将 <code>Type 0</code> 看作是一个由「小」或「普通」类型组成的宇宙。然后，<code>Type 1</code> 是一个更大的类型范围，其中包含 <code>Type 0</code> 作为一个元素，而 <code>Type 2</code> 是一个更大的类型范围，其中包含 <code>Type 1</code> 作为一个元素。这个列表是不确定的，所以对于每个自然数 <code>n</code> 都有一个 <code>Type n</code>。<code>Type</code> 是 <code>Type 0</code> 的缩写：</p>
+<p>可以将 <code>Type 0</code> 看作是一个由「小」或「普通」类型组成的宇宙。然后，<code>Type 1</code> 是一个更大的类型范围，其中包含 <code>Type 0</code> 作为一个元素，而 <code>Type 2</code> 是一个更大的类型范围，其中包含 <code>Type 1</code> 作为一个元素。这个列表是无限的，所以对于每个自然数 <code>n</code> 都有一个 <code>Type n</code>。<code>Type</code> 是 <code>Type 0</code> 的缩写：</p>
 <pre><code class="language-lean">#check Type
 #check Type 0
 </code></pre>

print.html

@@ -652,7 +652,7 @@ <h2 id="类型作为对象"><a class="header" href="#类型作为对象">类型
 that there is a ``Type n`` for every natural number ``n``. ``Type`` is
 an abbreviation for ``Type 0``:
 -->
-<p>可以将 <code>Type 0</code> 看作是一个由「小」或「普通」类型组成的宇宙。然后，<code>Type 1</code> 是一个更大的类型范围，其中包含 <code>Type 0</code> 作为一个元素，而 <code>Type 2</code> 是一个更大的类型范围，其中包含 <code>Type 1</code> 作为一个元素。这个列表是不确定的，所以对于每个自然数 <code>n</code> 都有一个 <code>Type n</code>。<code>Type</code> 是 <code>Type 0</code> 的缩写：</p>
+<p>可以将 <code>Type 0</code> 看作是一个由「小」或「普通」类型组成的宇宙。然后，<code>Type 1</code> 是一个更大的类型范围，其中包含 <code>Type 0</code> 作为一个元素，而 <code>Type 2</code> 是一个更大的类型范围，其中包含 <code>Type 1</code> 作为一个元素。这个列表是无限的，所以对于每个自然数 <code>n</code> 都有一个 <code>Type n</code>。<code>Type</code> 是 <code>Type 0</code> 的缩写：</p>
 <pre><code class="language-lean">#check Type
 #check Type 0
 </code></pre>