Enumerated Types

An unusual aspect of Kind, similar to other proof languages such as Idris and Coq, is that its built-in toolset is quite small. For example, instead of providing the usual range of primitive types (booleans, lists, strings, etc), Kind has only two primitive types (U60: unsigned 60-bit binary integers) and (F60: unsigned 60-bit binary floating point numbers) and offers a powerful mechanism for defining new data types from scratch, from which all these familiar types and more can be derived.

To demonstrate how the definition mechanism works, let's start with a simple example.