Closed Seasawher closed 1 week ago
迷ったのだが，
_root_
というコードは「expected command」というエラーになるので，_root_ はコマンド扱いではないと思う．local や noncomputable のような修飾子もそんなエラーは出さない．
「構文」カテゴリは対話的でないコマンドのためのカテゴリなので，namespace の説明に組み込むのが一貫性のあるアプローチだと思う．
namespace
迷ったのだが，
というコードは「expected command」というエラーになるので，
_root_はコマンド扱いではないと思う．local や noncomputable のような修飾子もそんなエラーは出さない．「構文」カテゴリは対話的でないコマンドのためのカテゴリなので，
namespaceの説明に組み込むのが一貫性のあるアプローチだと思う．