From 1a9154c63096a91552f238871d65da182d52efa8 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 19 May 2026 07:23:40 +0000
Subject: [PATCH 1/3] Initial plan


From f03297344857b40ac269873cca406fdf32a1fcb0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 19 May 2026 07:46:31 +0000
Subject: [PATCH 2/3] Explain variable inclusion difference between theorem and
 def

Agent-Logs-Url: https://github.com/lean-ja/lean-by-example/sessions/9a810955-8099-4b58-8947-e681218e6dda

Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
---
 LeanByExample/Declarative/Variable.lean | 30 +++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/LeanByExample/Declarative/Variable.lean b/LeanByExample/Declarative/Variable.lean
index d12f120d..1085b985 100644
--- a/LeanByExample/Declarative/Variable.lean
+++ b/LeanByExample/Declarative/Variable.lean
@@ -29,6 +29,36 @@ def isNil : Bool :=
 theorem nng_list_length : l.length ≥ 0 := by simp
 
 end variable1 --#
+
+/- ## theorem と def での取り込み基準の違い
+
+`theorem` は statement（型）に現れる変数だけを自動で引数にします。
+そのため、証明中でのみ使う外側の変数は `include` で明示的に取り込みます。
+-/
+namespace variable2 --#
+
+variable (n : Nat)
+
+/-⋆-//--
+error: unknown identifier 'n'
+-/
+#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
+
+end variable2 --#
+
 /- ## 再帰と variable
 
 `variable` コマンドで宣言された引数は、再帰呼び出しの中でも同じ値が使用されます。

From 813138243efdab329a5ac4f43f8a2f01ea3629f1 Mon Sep 17 00:00:00 2001
From: Codex <codex@openai.com>
Date: Mon, 25 May 2026 02:57:34 +0900
Subject: [PATCH 3/3] fix: clarify variable command example

---
 LeanByExample/Declarative/Variable.lean | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/LeanByExample/Declarative/Variable.lean b/LeanByExample/Declarative/Variable.lean
index 1085b985..30e0a8c4 100644
--- a/LeanByExample/Declarative/Variable.lean
+++ b/LeanByExample/Declarative/Variable.lean
@@ -32,31 +32,46 @@ end variable1 --#
 
 /- ## theorem と def での取り込み基準の違い
 
-`theorem` は statement（型）に現れる変数だけを自動で引数にします。
+`theorem` は定理の型に現れる変数だけを自動で引数にします。
 そのため、証明中でのみ使う外側の変数は `include` で明示的に取り込みます。
+一方で、`def` は本体に現れる変数も自動で引数にします。
 -/
 namespace variable2 --#
 
 variable (n : Nat)
 
 /-⋆-//--
-error: unknown identifier 'n'
+error: Unknown identifier `n`
+---
+error: Unknown identifier `n`
 -/
 #guard_msgs in --#
-theorem foo (m : Nat) : m = m := by
+theorem foo (m : Nat) : m = m :=
   have : n = n := by rfl
   rfl
 
-def foo' (m : Nat) : m = m := by
+def foo' (m : Nat) : m = m :=
   have : n = n := by rfl
   rfl
 
+/-⋆-//--
+info: variable2.foo' (n m : Nat) : m = m
+-/
+#guard_msgs in --#
+#check foo'
+
 include n
 
-theorem foo_included (m : Nat) : m = m := by
+theorem foo_included (m : Nat) : m = m :=
   have : n = n := by rfl
   rfl
 
+/-⋆-//--
+info: variable2.foo_included (n m : Nat) : m = m
+-/
+#guard_msgs in --#
+#check foo_included
+
 end variable2 --#
 
 /- ## 再帰と variable