構造・構成素の乱用は、一番よくやるやつ。M = (M, *, e) とか。コジュール接続だと:
- E = (E, S, ∇) where S = Γ(E)
- S = (E, S, ∇)
- ∇ = (E, S, ∇)
名前付き順序付きタプルを使って、 X = {v-bundle: E, sec-space, deriv: ∇} とすれば、
- X.v-bundle = E
- X.sec-space = S
- X.deriv = ∇
v-bundle, sec-space, deriv を構造の構成素名、または役割名と呼ぶ。出現順で番号付けるとすれば:
- X.1 = E
- X.2 = S
- X.3 = ∇
Coqと同様に、文脈型推論(出現する文脈の情報からの型推論)と強制グラフでオーバーロード解決が可能(たぶん)。
構造の定義のときに、構成素名〈constituent names〉と構成素順番〈constituent ordering〉を決める。乱用に使う強制アローを決めて、強制グラフを更新する。
用語法でも同じで、「V がベクトル空間である」から「(V, +, ・) がベクトル空間である」と読み替える。
同型・等値の乱用は、A B を A = B と書くこと。これについては、同値類に落として解釈できることもあるが、矛盾が出ないかを注意深くチェックしなくてはならないので、かなり危険。合理化は難しい。典型事例は、V** = V 。