scoped の例を，コマンドの不在を確認するように修正

-- #target をコマンドとして認識させる
-- 実装は与えない
syntax "#greet" : command

namespace Scoped
  -- scoped 付きで #greet コマンドにマクロとして実装を与える
  scoped macro "#greet" : command => `(#eval "hello, world!")

  -- その名前空間の中では使える
  #greet

end Scoped

-- 名前空間を抜けると使えなくなる
/-- error: elaboration function for '«command#greet»' has not been implemented -/
#guard_msgs in #greet

namespace Scoped
  -- 再び同じ名前空間を開くと使えるようになる
  #greet
end Scoped

lean-ja / lean-by-example

scoped の例を，コマンドの不在を確認するように修正 #392