Just met this symbol :<> in the dependently typed factorial section in the book "introduction to programming in ats": https://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/x3215.html
There seem to be no explanations before. My hypothesis is that it's the same as a single colon :
This strange syntax is used to indicate that a function is pure, that is, causing no effects when is called.