From f545f3b4ea17384753b8727781c5b1d6efdb63ae Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 15 Sep 2024 01:40:30 +0900
Subject: [PATCH] =?UTF-8?q?elab=20=E3=82=B3=E3=83=9E=E3=83=B3=E3=83=89?=
 =?UTF-8?q?=E4=BD=BF=E7=94=A8=E4=BE=8B=EF=BC=9Atada=20=E3=82=BF=E3=82=AF?=
 =?UTF-8?q?=E3=83=86=E3=82=A3=E3=82=AF=20Fixes=20#426?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Declarative/Elab.lean | 38 ++++++++++++++++++++++++++
 src/SUMMARY.md                         |  1 +
 2 files changed, 39 insertions(+)
 create mode 100644 Examples/Command/Declarative/Elab.lean

diff --git a/Examples/Command/Declarative/Elab.lean b/Examples/Command/Declarative/Elab.lean
new file mode 100644
index 00000000..54d48d09
--- /dev/null
+++ b/Examples/Command/Declarative/Elab.lean
@@ -0,0 +1,38 @@
+/- # elab
+
+`elab` コマンドは、構文に意味を与えるためのコマンドです。特定の構文の解釈を、手続きとして記述するときに使用されます。
+
+以下の例は、証明が終了したときに 🎉 でお祝いしてくれるタクティクを自作する例です。[^zulip]
+-/
+import Lean
+
+open Lean Elab Tactic Term
+
+elab "tada" : tactic => do
+  -- 未解決のゴールを List として取得する
+  let gs ← getUnsolvedGoals
+
+  -- ゴールが空なら 🎉 でお祝いする
+  if gs.isEmpty then
+    logInfo "Goals accomplished 🎉"
+  else
+    -- ゴールが残っているというメッセージを出す
+    reportUnsolvedGoals gs
+
+    -- エラーにする
+    throwAbortTactic
+
+/--
+error: unsolved goals
+⊢ True
+-/
+#guard_msgs in
+  example : True := by tada
+
+/-- info: Goals accomplished 🎉 -/
+#guard_msgs in
+  example : True := by
+    trivial
+    tada
+
+/- [^zulip]: Zulip のスレッド [new members > lean3 or 4?](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.203.20or.204.3F) からコード例を引用しています。-/
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index fed23bfe..b3220002 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -30,6 +30,7 @@
     - [declare_syntax_cat: 構文カテゴリ](./Command/Declarative/DeclareSyntaxCat.md)
     - [def: 関数などを定義する](./Command/Declarative/Def.md)
     - [deriving: インスタンス自動生成](./Command/Declarative/Deriving.md)
+    - [elab: 構文に意味を与える](./Command/Declarative/Elab.md)
     - [example: 名前をつけずに証明](./Command/Declarative/Example.md)
     - [export: 現在の名前空間に追加](./Command/Declarative/Export.md)
     - [inductive: 帰納型を定義する](./Command/Declarative/Inductive.md)