Tipos Enumerados

Um aspecto incomum do Kind, similar a outras linguagens de prova como Idris e Coq, é que o seu conjunto de ferramentas built-in é bastante pequeno. Por exemplo, ao invés de fornecer o leque usual de tipos primitivos (booleanos, listas, strings, etc), Kind tem apenas dois tipos primitivos (U60: números inteiros em 60 bits binários, sem sinal) e (F60: números de ponto flutuante em 60 bits binários, sem sinal) e oferece um mecanismo poderoso para definir novos tipos de dados do zero, do qual pode-se derivar todos esses tipos já familiares e outros.

Para demonstrar como funciona o mecanismo de definição, vamos começar com um exemplo simples.