elab コマンド使用例：tada タクティク

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) からコード例を引用しています。-/

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)