要素\(a\)の型が\(A\)であることを明示するときは\(a:A\)と書く。