Skip to main content

Built-in Types

nat64-bit natural numbers
byte8-bit natural numbers
stringUTF-8 encoded strings
[T]lists of elements of type T
{ field₁ : T₁, ..., fieldₙ : Tₙ }a record with zero or more named fields
{ field₁ : T₁ | ... | fieldₙ : Tₙ }a sum (union) type with one or more named alternatives
Pa reference to a fact of predicate P
boolthe boolean type with values true and false
maybe Tan optional value of type T
enum { name₁ | ... | nameₙ }exactly one of the symbols name₁..nameₙ