Skip to main content

Built-in Types

TypeMeaning
nat64-bit natural numbers
byte8-bit natural numbers
stringUTF-8 encoded strings
[T]lists of elements of type T
set T set 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ā‚™