deploy: 1726579

getting-to-know/structures.html

@@ -141,11 +141,13 @@ <h1 class="menu-title">Functional Programming in Lean 日本語訳</h1>
 
                 <div id="content" class="content">
                     <main>
-                        <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.
+                        <!-- # Structures -->
+<h1 id="構造体"><a class="header" href="#構造体">構造体</a></h1>
+<!-- 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.
-In that case, it can be convenient to group these simpler components together into a single &quot;package&quot;, which can then be given a meaningful name.
-In Lean, this is done using <em>structures</em>, which are analogous to <code>struct</code>s in C or Rust and <code>record</code>s in C#.</p>
+In that case, it can be convenient to group these simpler components together into a single "package", which can then be given a meaningful name.
+In Lean, this is done using _structures_, which are analogous to `struct`s in C or Rust and `record`s in C#. -->
+<p>プログラムを書く最初のステップは，通常，問題領域の概念を確認し，それをコードで適切に表現することです．ドメイン概念は，他のもっと単純な概念の集まりであることがあります．そういったとき，単純な構成要素をひとつの「パッケージ」にまとめ，意味のある名前をつけると便利でしょう．Lean では，それは構造体(structure)によって実現できます．これは Rust や C の <code>struct</code>，C# でいう <code>record</code> に対応するものです．</p>
 <p>Defining a structure introduces a completely new type to Lean that can't be reduced to any other type.
 This is useful because multiple structures might represent different concepts that nonetheless contain the same data.
 For instance, a point might be represented using either Cartesian or polar coordinates, each being a pair of floating-point numbers.

print.html

@@ -689,11 +689,13 @@ <h3 id="よくあるエラー-1"><a class="header" href="#よくあるエラー-
 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>
-<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.
+<div style="break-before: page; page-break-before: always;"></div><!-- # Structures -->
+<h1 id="構造体"><a class="header" href="#構造体">構造体</a></h1>
+<!-- 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.
-In that case, it can be convenient to group these simpler components together into a single &quot;package&quot;, which can then be given a meaningful name.
-In Lean, this is done using <em>structures</em>, which are analogous to <code>struct</code>s in C or Rust and <code>record</code>s in C#.</p>
+In that case, it can be convenient to group these simpler components together into a single "package", which can then be given a meaningful name.
+In Lean, this is done using _structures_, which are analogous to `struct`s in C or Rust and `record`s in C#. -->
+<p>プログラムを書く最初のステップは，通常，問題領域の概念を確認し，それをコードで適切に表現することです．ドメイン概念は，他のもっと単純な概念の集まりであることがあります．そういったとき，単純な構成要素をひとつの「パッケージ」にまとめ，意味のある名前をつけると便利でしょう．Lean では，それは構造体(structure)によって実現できます．これは Rust や C の <code>struct</code>，C# でいう <code>record</code> に対応するものです．</p>
 <p>Defining a structure introduces a completely new type to Lean that can't be reduced to any other type.
 This is useful because multiple structures might represent different concepts that nonetheless contain the same data.
 For instance, a point might be represented using either Cartesian or polar coordinates, each being a pair of floating-point numbers.