Skip to main content

Number Types

The following diagram illustrates the hierarchy of numeric types supported by Caesar.

An arrow from a type to another type indicates that it is a subtype and that a value can be converted into the supertype. This is done automatically by Caesar when appropriate.

Mathematical Number Types

Caesar supports various number types that are not restricted by a finite bit size. Therefore, all of these types have infinitely many values.


Unsigned integers, i.e. values 0, 1, 2, and so on.

This type was previously called `Uint`. For the moment, Caesar also accepts this name.


Signed integers.


Unsigned real numbers, i.e. values x ∈ ℝ such that x ≥ 0.

This is the type of fraction expressions a/b where a and b are unsigned integer literals, as well as decimals such as 3.14.


Actual real numbers!


Extended unsigned real numbers. This type includes all values from the UReal type and also allows the value .

This type admits a Heyting algebra and can be used as a verification domain.

This type was previously called Realplus. For the moment, Caesar also accepts this name.