inductiveな型と同名の名前空間を定義して、そのなかにstuffを入れる。以下は実例： structure Parser.Category namespace Parser.Category /- ... ... -/ end Parser.CategoryLeanのキモのひとつは、名前空間／シンボル空間の構造と相互作用を理解すること。