variable 解説に theorem/def の変数取り込み差分と include の実例を追加

[Copilot]

variable の外側宣言が theorem と def で同様に取り込まれるように見える一方、実際は基準が異なるため混乱が起きていました。theorem は statement 基準、def は本体での使用も含むことを、失敗例と修正例で明示しました。

• 変更内容: variable ページの挙動説明を補強

  • LeanByExample/Declarative/Variable.lean に theorem / def の取り込み基準の違いを説明する節を追加
  • theorem で証明中のみ使う外側変数は自動取り込みされない点を明記
  • include n を使って theorem 側で明示的に取り込むパターンを追加

• 変更内容: 挙動をそのまま再現できる最小例を追加

  • #guard_msgs で unknown identifier 'n' を検証する失敗例
  • 同じ文脈で def が通る対比例
  • include n 後に theorem が通る成功例

variable (n : Nat)

#guard_msgs in
theorem foo (m : Nat) : m = m := by
  have : n = n := by rfl
  rfl

def foo' (m : Nat) : m = m := by
  have : n = n := by rfl
  rfl

include n
theorem foo_included (m : Nat) : m = m := by
  have : n = n := by rfl
  rfl