Clarify protected behavior for nested namespaces

[Copilot]

protected の説明が「フルネームの強制」になっていましたが、ネストした名前空間では実際の挙動とずれていました。protected が禁止するのは短い名前での参照であり、状況によっては最も近い名前空間名までの修飾で参照できます。

• 説明の修正

  • LeanByExample/Modifier/Protected.lean の冒頭説明を更新
  • 「必ずフルネーム」ではなく、「短い名前では参照できず、ネスト時は最も近い名前空間名までは必要」という表現に調整

• ネストした名前空間の例を追加

  • protected な定義が、同じスコープでは foo で参照できず、Inner.foo では参照できる例を追加
  • 外側のスコープでは Outer.Inner.foo が必要になることも併記

• 見出しの表現を調整

  • SUMMARY.lean の項目名を フルネームを強制する から 名前空間名の省略を防ぐ に更新

例:

namespace Outer
  namespace Inner
    protected def foo := 42

    #check_failure foo
    #check Inner.foo
  end Inner

  #check_failure foo
  #check Inner.foo
end Outer

#check Outer.Inner.foo