deploy: 58225c3

lean-ja · Oct 21, 2023 · 6735a1b · 6735a1b
1 parent b2ee76d
commit 6735a1b
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/getting-to-know/functions-and-definitions.html b/getting-to-know/functions-and-definitions.html
@@ -292,7 +292,7 @@ <h3 id="よくあるエラー"><a class="header" href="#よくあるエラー">
 Definitions that are to be unfolded are called _reducible_.
 Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand.
 Definitions produced with `abbrev` are marked as reducible. -->
-<p>舞台裏では, オーバーロードの解決時に, 展開可能(unfoldable)であると内部でマークされる定義もあれば，そうでない定義もあります．展開される定義は <em>reducible</em> と呼ばれます．Lean をスケールさせるためには，定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると, 型が非常に大きくなり, 機械が処理するのに時間がかかりますし, ユーザーにとっても理解しづらいものになります．<code>abbrev</code> で生成された定義は reducible であるとマークされます．</p>
+<p>舞台裏では, オーバーロードの解決時に, 展開可能(unfoldable)であると内部でマークされる定義もあれば，そうでない定義もあります．展開される定義は <em>reducible</em> と呼ばれます．Lean をスケールさせるためには，定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると, 型が非常に大きくなり, 機械が処理するのに時間がかかりますし, ユーザにとっても理解しづらいものになります．<code>abbrev</code> で生成された定義は reducible であるとマークされます．</p>
 
                     </main>
 

diff --git a/print.html b/print.html
@@ -685,7 +685,7 @@ <h3 id="よくあるエラー-1"><a class="header" href="#よくあるエラー-
 Definitions that are to be unfolded are called _reducible_.
 Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand.
 Definitions produced with `abbrev` are marked as reducible. -->
-<p>舞台裏では, オーバーロードの解決時に, 展開可能(unfoldable)であると内部でマークされる定義もあれば，そうでない定義もあります．展開される定義は <em>reducible</em> と呼ばれます．Lean をスケールさせるためには，定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると, 型が非常に大きくなり, 機械が処理するのに時間がかかりますし, ユーザーにとっても理解しづらいものになります．<code>abbrev</code> で生成された定義は reducible であるとマークされます．</p>
+<p>舞台裏では, オーバーロードの解決時に, 展開可能(unfoldable)であると内部でマークされる定義もあれば，そうでない定義もあります．展開される定義は <em>reducible</em> と呼ばれます．Lean をスケールさせるためには，定義の展開可能性のコントロールが不可欠です：すべての定義を完全に展開すると, 型が非常に大きくなり, 機械が処理するのに時間がかかりますし, ユーザにとっても理解しづらいものになります．<code>abbrev</code> で生成された定義は reducible であるとマークされます．</p>
 <div style="break-before: page; page-break-before: always;"></div><h1 id="structures"><a class="header" href="#structures">Structures</a></h1>
 <p>The first step in writing a program is usually to identify the problem domain's concepts, and then find suitable representations for them in code.
 Sometimes, a domain concept is a collection of other, simpler, concepts.

diff --git a/searchindex.js b/searchindex.js
diff --git a/searchindex.json b/searchindex.json