From 4f5531f5791debac2d668fdbb432c3b88ce897f4 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 10 Oct 2023 19:58:32 +0900
Subject: [PATCH] =?UTF-8?q?guard=5Fhyp=20=E3=82=92=E8=BF=BD=E5=8A=A0?=
 =?UTF-8?q?=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples.lean          |  1 +
 Examples/GuardHyp.lean |  9 +++++++++
 src/SUMMARY.md         |  1 +
 src/guard_hyp.md       | 11 +++++++++++
 4 files changed, 22 insertions(+)
 create mode 100644 Examples/GuardHyp.lean
 create mode 100644 src/guard_hyp.md

diff --git a/Examples.lean b/Examples.lean
index 985f105a..739fb949 100644
--- a/Examples.lean
+++ b/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
diff --git a/Examples/GuardHyp.lean b/Examples/GuardHyp.lean
new file mode 100644
index 00000000..433e7e64
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index a051041e..dee641da 100644
--- a/src/SUMMARY.md
+++ b/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)
diff --git a/src/guard_hyp.md b/src/guard_hyp.md
new file mode 100644
index 00000000..cf1d0505
--- /dev/null
+++ b/src/guard_hyp.md
@@ -0,0 +1,11 @@
+# guard_hyp
+
+needs: `import Std.Tactic.GuardExpr`
+
+`guard_hyp` は，ローカルコンテキストにある命題を確認するタクティクです．指定した仮定が存在すれば成功し，そうでなければ失敗します．
+
+```lean
+{{#include ../Examples/GuardHyp.lean:first}}
+```
+
+通常の証明で使うことはあまりないかもしれません．このタクティクリストでは，ローカルコンテキストの変化を説明するために使用することがあります．
\ No newline at end of file