From d7573348bf34570c3439f2af19b06e259b5b68f2 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 1 Sep 2024 09:51:00 +0900
Subject: [PATCH] =?UTF-8?q?protected=20=E3=81=AE=E3=82=B3=E3=83=BC?=
 =?UTF-8?q?=E3=83=89=E3=81=AE=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Declarative/Protected.lean | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/Examples/Command/Declarative/Protected.lean b/Examples/Command/Declarative/Protected.lean
index c2bf82f5..5923e089 100644
--- a/Examples/Command/Declarative/Protected.lean
+++ b/Examples/Command/Declarative/Protected.lean
@@ -52,6 +52,17 @@ end Foo
 
 /- `Foo.baz` を `protected` として宣言しておけば、他の名前空間に影響を及ぼさなくなります。-/
 
+protected def Foo.baz := "hello"
+
+def baz := "world"
+
+namespace Foo
+
+-- 単に baz と書いたらルートの baz が参照される
+#guard baz = "world"
+
+end Foo
+
 /- ## protected def 以外の用法
 
 `def` コマンドに対してだけでなく、[`indudctive`](./Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/
@@ -81,14 +92,14 @@ structure Sample where
   protected mk ::
 
   bar : Nat
-  protected baz : String
+  protected hoge : String
 
 open Sample
 
 -- 名前空間を開いているので bar には短い名前でアクセスできる
 #check bar
 
--- baz には短い名前でアクセスできない
-#check_failure baz
+-- hoge には短い名前でアクセスできない
+#check_failure hoge
 
 end --#