Dafny tem as seguintes maneiras de declarar tipos que suportam igualdade.
T(==)
Mas existe uma maneira de especificar o tipo que suporta ordenação ( <, <=, >, >=) etc.?
AskOverflow.Dev
O Dafny não suporta sobrecarga de operadores. No entanto, você pode definir seus próprios predicados para suportar ordenação em seu tipo de dados. Se você fizer disso um módulo, poderá abstrair a comparação de ordenação real também. Então, mais tarde, quando tiver um tipo nativo que suporte esses operadores, você pode simplesmente fornecer a implementação das operações como uma instância de módulo.
Houve uma ótima postagem no blog com um exemplo, que agora só consigo encontrar na máquina do Wayback aqui