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

LeanByExample/Declarative/Variable.lean

@@ -29,6 +29,51 @@ def isNil : Bool :=
 theorem nng_list_length : l.length ≥ 0 := by simp
 
 end variable1 --#
+
+/- ## theorem と def での取り込み基準の違い
+
+`theorem` は定理の型に現れる変数だけを自動で引数にします。
+そのため、証明中でのみ使う外側の変数は `include` で明示的に取り込みます。
+一方で、`def` は本体に現れる変数も自動で引数にします。
+-/
+namespace variable2 --#
+
+variable (n : Nat)
+
+/-⋆-//--
+error: Unknown identifier `n`
+---
+error: Unknown identifier `n`
+-/
+#guard_msgs in --#
+theorem foo (m : Nat) : m = m :=
+  have : n = n := by rfl
+  rfl
+
+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 :=
+  have : n = n := by rfl
+  rfl
+
+/-⋆-//--
+info: variable2.foo_included (n m : Nat) : m = m
+-/
+#guard_msgs in --#
+#check foo_included
+
+end variable2 --#
+
 /- ## 再帰と variable
 
 `variable` コマンドで宣言された引数は、再帰呼び出しの中でも同じ値が使用されます。