deploy: 300432c

index.html

@@ -177,6 +177,9 @@ <h1 class="menu-title">Lean4 タクティク逆引きリスト</h1>
                         <h1 id="lean4-タクティク逆引きリスト"><a class="header" href="#lean4-タクティク逆引きリスト">Lean4 タクティク逆引きリスト</a></h1>
 <p>「普段の数学を Lean でどうやって実現するんだろう」という疑問に答えるために，よく使うタクティクをユースケースから逆引きできるようにまとめたリストです．</p>
 <p>なお，タクティクの説明に付記している名前の由来についての説明は公式に説明があったものではなく，あくまで憶測であることをお断りしておきます．</p>
+<h2 id="オプションについて"><a class="header" href="#オプションについて">オプションについて</a></h2>
+<p>タクティクによっては，オプションを設定することで挙動を変更することができます．オプションの設定には，<code>set_option</code> を使用します．たとえば，<code>set_option warningAsError true</code> と書くと，warning(警告) がエラーとして扱われるようになります．</p>
+<p>使用できるオプションの一覧は <code>#help option</code> で確認することができます．</p>
 <h2 id="リンク集"><a class="header" href="#リンク集">リンク集</a></h2>
 <ul>
 <li>

print.html

@@ -178,6 +178,9 @@ <h1 class="menu-title">Lean4 タクティク逆引きリスト</h1>
                         <h1 id="lean4-タクティク逆引きリスト"><a class="header" href="#lean4-タクティク逆引きリスト">Lean4 タクティク逆引きリスト</a></h1>
 <p>「普段の数学を Lean でどうやって実現するんだろう」という疑問に答えるために，よく使うタクティクをユースケースから逆引きできるようにまとめたリストです．</p>
 <p>なお，タクティクの説明に付記している名前の由来についての説明は公式に説明があったものではなく，あくまで憶測であることをお断りしておきます．</p>
+<h2 id="オプションについて"><a class="header" href="#オプションについて">オプションについて</a></h2>
+<p>タクティクによっては，オプションを設定することで挙動を変更することができます．オプションの設定には，<code>set_option</code> を使用します．たとえば，<code>set_option warningAsError true</code> と書くと，warning(警告) がエラーとして扱われるようになります．</p>
+<p>使用できるオプションの一覧は <code>#help option</code> で確認することができます．</p>
 <h2 id="リンク集"><a class="header" href="#リンク集">リンク集</a></h2>
 <ul>
 <li>
@@ -993,9 +996,16 @@ <h2 id="nth_rewrite"><a class="header" href="#nth_rewrite">nth_rewrite</a></h2>
     apply hgfinj
     simp_all only [comp_apply]
 </code></pre>
-<h2 id="補足-4"><a class="header" href="#補足-4">補足</a></h2>
 <p>より詳細には，検索タクティク <code>X</code> があり，その提案内容が <code>Try this: Y</code> だったとき，<code>X says</code> とすると <code>says</code> は <code>Try this: Y</code> の代わりに <code>Try this: X says Y</code> という提案を infoview 上で出します．それをクリックすると，<code>X says</code> の内容が <code>X says Y</code> で置換されます．そして，<code>X says Y</code> が実行されるときには <code>X</code> は飛ばされます．</p>
-<p>なお，<code>X says Y</code> の <code>Y</code> のところに，実際には提案されていないタクティクを入れてもエラーにはなりません．したがって <code>X says Y</code> は，<code>X</code> の提案内容の中に <code>Try this: Y</code> があることを保証しません．</p>
+<h2 id="オプション"><a class="header" href="#オプション">オプション</a></h2>
+<ul>
+<li>
+<p><code>says.verify : Bool</code> : <code>true</code> にすると，<code>X says Y</code> の <code>Y</code> のところに，実際には提案されていないタクティクを入れたときにエラーになります．</p>
+</li>
+<li>
+<p><code>says.no_verify_in_CI : Bool</code> : <code>true</code> にすると，CI 環境で <code>X says Y</code> の <code>Y</code> の部分が実際に提案されている内容と一致するかのチェックが走らなくなります．</p>
+</li>
+</ul>
 <div style="break-before: page; page-break-before: always;"></div><h1 id="show"><a class="header" href="#show">show</a></h1>
 <p><code>show P</code> は, ゴールの中に <code>⊢ P</code> があるときにそれをメインのゴールにします．</p>
 <p>たとえば，証明中にこれから示すべきことを明示し，コードを読みやすくする目的で使うことができます．</p>

says.html

@@ -191,9 +191,16 @@ <h1 id="says"><a class="header" href="#says">says</a></h1>
     apply hgfinj
     simp_all only [comp_apply]
 </code></pre>
-<h2 id="補足"><a class="header" href="#補足">補足</a></h2>
 <p>より詳細には，検索タクティク <code>X</code> があり，その提案内容が <code>Try this: Y</code> だったとき，<code>X says</code> とすると <code>says</code> は <code>Try this: Y</code> の代わりに <code>Try this: X says Y</code> という提案を infoview 上で出します．それをクリックすると，<code>X says</code> の内容が <code>X says Y</code> で置換されます．そして，<code>X says Y</code> が実行されるときには <code>X</code> は飛ばされます．</p>
-<p>なお，<code>X says Y</code> の <code>Y</code> のところに，実際には提案されていないタクティクを入れてもエラーにはなりません．したがって <code>X says Y</code> は，<code>X</code> の提案内容の中に <code>Try this: Y</code> があることを保証しません．</p>
+<h2 id="オプション"><a class="header" href="#オプション">オプション</a></h2>
+<ul>
+<li>
+<p><code>says.verify : Bool</code> : <code>true</code> にすると，<code>X says Y</code> の <code>Y</code> のところに，実際には提案されていないタクティクを入れたときにエラーになります．</p>
+</li>
+<li>
+<p><code>says.no_verify_in_CI : Bool</code> : <code>true</code> にすると，CI 環境で <code>X says Y</code> の <code>Y</code> の部分が実際に提案されている内容と一致するかのチェックが走らなくなります．</p>
+</li>
+</ul>
 
                     </main>