タクティク衛生(tactic hygiene)の例: タクティクの中で識別子を導入する

[Seasawher]

/- ## タクティクの中で識別子を導入する例 -/

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 in

macro "my_intro'" : tactic => `(tactic| intro h)

example (P : Prop) : P → P := by
  my_intro'

  -- 衛生的ではないので、`h : P` が使えてしまう
  exact h