Skip to content

Commit

Permalink
deploy: ac33d70
Browse files Browse the repository at this point in the history
  • Loading branch information
@Seasawher
Seasawher committed Sep 22, 2023
1 parent 59057fd commit 20865b2
Show file tree
Hide file tree
Showing 35 changed files with 282 additions and 38 deletions.
2 changes: 1 addition & 1 deletion 404.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@

<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
Expand Down
2 changes: 1 addition & 1 deletion aesop.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@

<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html" class="active">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html" class="active">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
Expand Down
2 changes: 1 addition & 1 deletion apply.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@

<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<div class="sidebar-scrollbox">
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html" class="active">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
<ol class="chapter"><li class="chapter-item expanded affix "><a href="index.html">Lean4 タクティク逆引きリスト</a></li><li class="spacer"></li><li class="chapter-item expanded "><a href="aesop.html">aesop: ルーチン自動化</a></li><li class="chapter-item expanded "><a href="apply.html" class="active">apply: 含意→を使う</a></li><li class="chapter-item expanded "><a href="apply_question.html">apply?: ライブラリ検索</a></li><li class="chapter-item expanded "><a href="assumption.html">assumption: 仮定をそのまま使う</a></li><li class="chapter-item expanded "><a href="by_cases.html">by_cases: 排中律</a></li><li class="chapter-item expanded "><a href="by_contra.html">by_contra: 背理法</a></li><li class="chapter-item expanded "><a href="by.html">by: タクティクモードに入る</a></li><li class="chapter-item expanded "><a href="calc.html">calc: 計算モードに入る</a></li><li class="chapter-item expanded "><a href="cases.html">cases: 論理和∨を使う</a></li><li class="chapter-item expanded "><a href="constructor.html">constructor: 論理積∧を示す</a></li><li class="chapter-item expanded "><a href="contradiction.html">contradiction: 矛盾</a></li><li class="chapter-item expanded "><a href="conv.html">conv: 変換モードに入る</a></li><li class="chapter-item expanded "><a href="done.html">done: 証明終了を宣言</a></li><li class="chapter-item expanded "><a href="exact.html">exact: 証明を直接構成</a></li><li class="chapter-item expanded "><a href="exists.html">exists: 存在∃を示す</a></li><li class="chapter-item expanded "><a href="ext.html">ext: 外延性を使う</a></li><li class="chapter-item expanded "><a href="funext.html">funext: 関数等式を示す</a></li><li class="chapter-item expanded "><a href="have.html">have: 補題を用意する</a></li><li class="chapter-item expanded "><a href="induction.html">induction: 帰納法</a></li><li class="chapter-item expanded "><a href="intro.html">intro: 含意→や全称∀を示す</a></li><li class="chapter-item expanded "><a href="left_right.html">left, right: 論理和∨を示す</a></li><li class="chapter-item expanded "><a href="rel.html">rel: 不等式を使う</a></li><li class="chapter-item expanded "><a href="rfl.html">rfl: 定義そのまま</a></li><li class="chapter-item expanded "><a href="ring.html">ring: 環の等式を示す</a></li><li class="chapter-item expanded "><a href="rw.html">rw: 同値変形</a></li><li class="chapter-item expanded "><a href="show.html">show: 示すべきことを宣言</a></li><li class="chapter-item expanded "><a href="simp.html">simp: 簡約</a></li><li class="chapter-item expanded "><a href="sorry.html">sorry: 証明したことにする</a></li><li class="chapter-item expanded "><a href="suffices.html">suffices: 十分条件に帰着</a></li><li class="chapter-item expanded "><a href="trivial.html">trivial: 自明</a></li></ol>
</div>
<div id="sidebar-resize-handle" class="sidebar-resize-handle"></div>
</nav>
Expand Down
Loading

0 comments on commit 20865b2

Please sign in to comment.