今度はattribute

attributeもテクニカルタームらしい。オプションとかアノテーションとかに近いものらしい。定理に対して、なんらかの付加情報を付ける働きがあるようだ。

構文範疇にattributeがある。attributeは、'[' 名前 引数のカンマ区切り並び ']' の形で、ブラケットだから、IDLのアノテーション（だっけ？）と同じと言えば同じだ。print_attributesコマンドがある。