unimath-symbols.pdf, the open colon ⦂ (U+02982), called the Z notation type colon, is declared as
\mathbin. As far as I know, you use this type colon as demonstrated in the following example. The lines
x ⦂ int f ⦂ int → int
declare a nullary symbol
x of integer type (or integer sort, depending on your vocabulary) and a unary function symbol
f of type
int → int. Therefore, the open colon ⦂ is a relation symbol, implying that it should be
\mathrel. See, e.g., http://czt.sourceforge.net/latex/z/czt-guide.pdf (though as of today, this symbol is probably not used in Z).
- Any idea why the symbol was listed as
- Did we hit a documentation / interpretation error?
UPDATE: After reading Short Math Guide for LaTeX, I'm no more sure that the spacing around the fat open colon must be symmetrical. Symmetrical spacing was just an approach of using
: for the typing judgements so far (which I and apparently thousands of other people used for many years) and an approach of a few other sources, e.g., Formal Specification -- Z Notation -- Syntax, Type and Semantics. So, if someone has a strong counter-opinion on this, he/she please feel free to advocate for
\mathpunct. But in any case,
\mathbin is wrong.