deploy: 10a6c38

print.html

@@ -782,6 +782,32 @@ <h2 id="補足-1"><a class="header" href="#補足-1">補足</a></h2>
 
   exact hP
 </code></pre>
+<h2 id="constructor-との関連"><a class="header" href="#constructor-との関連">constructor との関連</a></h2>
+<p><code>refine</code> は <a href="./constructor.html">constructor</a> の代わりに使うこともできます．実際 <code>refine</code> は <code>constructor</code> よりも柔軟で，<code>⊢ P ∧ Q ∧ R</code> のような形のゴールは <code>constructor</code> よりも簡潔に分割できます．</p>
+<pre><code class="language-lean">example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+  -- ゴールを３つに分割する
+  refine ⟨?_, ?_, ?_⟩
+
+  · show P
+    exact hP
+  · show Q
+    exact hQ
+  · show R
+    exact hR
+
+-- `constructor` を使った場合
+-- 一度に２つのゴールに分割することしかできない
+example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+  constructor
+  · show P
+    exact hP
+  · show Q ∧ R
+    constructor
+    · show Q
+      exact hQ
+    · show R
+      exact hR
+</code></pre>
 <div style="break-before: page; page-break-before: always;"></div><h1 id="rel"><a class="header" href="#rel">rel</a></h1>
 <p>needs: <code>import Mathlib.Tactic.GCongr</code></p>
 <p>named after: 関係(relation)</p>

refine.html

@@ -185,6 +185,32 @@ <h1 id="refine"><a class="header" href="#refine">refine</a></h1>
 
   exact hP
 </code></pre>
+<h2 id="constructor-との関連"><a class="header" href="#constructor-との関連">constructor との関連</a></h2>
+<p><code>refine</code> は <a href="./constructor.html">constructor</a> の代わりに使うこともできます．実際 <code>refine</code> は <code>constructor</code> よりも柔軟で，<code>⊢ P ∧ Q ∧ R</code> のような形のゴールは <code>constructor</code> よりも簡潔に分割できます．</p>
+<pre><code class="language-lean">example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+  -- ゴールを３つに分割する
+  refine ⟨?_, ?_, ?_⟩
+
+  · show P
+    exact hP
+  · show Q
+    exact hQ
+  · show R
+    exact hR
+
+-- `constructor` を使った場合
+-- 一度に２つのゴールに分割することしかできない
+example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
+  constructor
+  · show P
+    exact hP
+  · show Q ∧ R
+    constructor
+    · show Q
+      exact hQ
+    · show R
+      exact hR
+</code></pre>
 
                     </main>