guard_hyp を追加する

Examples.lean

@@ -14,6 +14,7 @@ import Examples.Exact
 import Examples.Exists
 import Examples.Ext
 import Examples.Funext
+import Examples.GuardHyp
 import Examples.Have
 import Examples.Induction
 import Examples.Intro

Examples/GuardHyp.lean

@@ -0,0 +1,9 @@
+import Std.Tactic.GuardExpr
+
+-- ANCHOR: first
+example (hP : P) : P := by
+  -- 現在ローカルコンテキストにある命題を確認できる
+  guard_hyp hP : P
+
+  exact hP
+-- ANCHOR_END: first

src/SUMMARY.md

@@ -23,6 +23,7 @@
 - [exists: 存在∃を示す](./exists.md)
 - [ext: 外延性を使う](./ext.md)
 - [funext: 関数等式を示す](./funext.md)
+- [guard_hyp: 仮定や補題を確認](./guard_hyp.md)
 - [have: 補題を用意する](./have.md)
 - [induction: 帰納法](./induction.md)
 - [intro: 含意→や全称∀を示す](./intro.md)

src/guard_hyp.md

@@ -0,0 +1,11 @@
+# guard_hyp
+
+needs: `import Std.Tactic.GuardExpr`
+
+`guard_hyp` は，ローカルコンテキストにある命題を確認するタクティクです．指定した仮定が存在すれば成功し，そうでなければ失敗します．
+
+```lean
+{{#include ../Examples/GuardHyp.lean:first}}
+```
+
+通常の証明で使うことはあまりないかもしれません．このタクティクリストでは，ローカルコンテキストの変化を説明するために使用することがあります．