From fb54a00f16c5dec58207f0bb90ab52ba3f5c8bcd Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 30 Dec 2024 23:20:41 +0900
Subject: [PATCH] =?UTF-8?q?linter=20=E3=82=A8=E3=83=A9=E3=83=BC=E3=81=8C?=
 =?UTF-8?q?=E8=A8=AD=E5=AE=9A=E3=82=92=E8=B2=AB=E9=80=9A=E3=81=99=E3=82=8B?=
 =?UTF-8?q?=20Fixes=20#1247?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/Ring.lean | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/LeanByExample/Tactic/Ring.lean b/LeanByExample/Tactic/Ring.lean
index 2caf695c..afa8ed73 100644
--- a/LeanByExample/Tactic/Ring.lean
+++ b/LeanByExample/Tactic/Ring.lean
@@ -53,6 +53,32 @@ example {n : Nat} : n - n + n = n := by
 
   simp
 
+/- 実際、`ring` タクティクは失敗すると常に `ring_nf` を提案するようなマクロとして定義されています。 -/
+
+/-- `#expand` の入力に渡すための構文カテゴリ -/
+syntax macro_stx := command <|> tactic <|> term
+
+open Lean in
+
+/-- マクロを展開するコマンド -/
+elab "#expand " t:macro_stx : command => do
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
+  match ← Elab.liftMacroM <| Macro.expandMacro? t with
+  | none => logInfo m!"Not a macro"
+  | some t => logInfo m!"{t}"
+
+-- マクロ展開の中に `try_this ring_nf` が含まれる
+/--
+info: first
+| ring1
+| try_this ring_nf
+-/
+#guard_msgs (info, drop warning) in
+  #expand ring
+
 /- ## カスタマイズ
 
 新たに型 `R : Type` に対して `ring` タクティクが利用できるようにするためには、`R` を `CommSemiring` または `CommRing` のインスタンスにします。