型名と名前空間名

inductiveな型と同名の名前空間を定義して、そのなかにstuffを入れる。以下は実例：

structure Parser.Category

namespace Parser.Category

/- ...
  ...
-/
end Parser.Category

Leanのキモのひとつは、名前空間／シンボル空間の構造と相互作用を理解すること。