From acd91f31eeaa517dfb0c9950ae01426a40b31bec Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 4 Oct 2024 00:27:42 +0900
Subject: [PATCH] =?UTF-8?q?=E3=82=BF=E3=82=AF=E3=83=86=E3=82=A3=E3=82=AF?=
 =?UTF-8?q?=E3=81=AE=E4=B8=AD=E3=81=A7=E8=AD=98=E5=88=A5=E5=AD=90=E3=82=92?=
 =?UTF-8?q?=E5=B0=8E=E5=85=A5=E3=81=99=E3=82=8B=E4=BE=8B=E3=82=92=E8=BF=BD?=
 =?UTF-8?q?=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

see #669
---
 Examples/Option/Hygine.lean | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/Examples/Option/Hygine.lean b/Examples/Option/Hygine.lean
index bf4e7505..977192b4 100644
--- a/Examples/Option/Hygine.lean
+++ b/Examples/Option/Hygine.lean
@@ -22,10 +22,38 @@ set_option hygiene false
 /-- マクロ衛生が無効になった定数関数マクロ -/
 macro "const'" e:term : term => `(fun x => $e)
 
--- 引数の値が同じでも、識別子の名前によって値が変わるようになる。
+-- 引数の値が同じでも、識別子の名前によって値が変わるようになってしまった。
 -- これはマクロの中で使用されている変数名も `x` であるため。
 #guard (const' x) 0 = 0
 #guard (const' y) 0 = 42
 
 end --#
-/-  -/
+/- ## タクティクにおけるマクロ衛生
+
+タクティクで導入される識別子についても、実行時の環境にある識別子と衝突しないようにする機能が Lean にはあります。
+-/
+section --#
+
+macro "my_intro" : tactic => `(tactic| intro h)
+
+example (P : Prop) : P → P := by
+  my_intro
+
+  -- `h : P` がマクロ展開によって導入されはするが、
+  -- 死んでいるので使えない
+  fail_if_success exact h
+
+  assumption
+
+-- マクロ衛生を保つ機能を無効にする
+set_option hygiene false
+
+macro "my_intro'" : tactic => `(tactic| intro h)
+
+example (P : Prop) : P → P := by
+  my_intro'
+
+  -- `h : P` が使えてしまう
+  exact h
+
+end --#