Arithmetic

Naturals

The most basic type of number in Vehicle are the natural numbers. The type of natural numbers is written as Nat.

The available operations over naturals are:

Operation	Symbol	Type	Example
Addition	+	Nat -> Nat -> Nat	x + y
Multiplication	*	Nat -> Nat -> Nat	x * y
Division	/	Nat -> Nat -> Rat	x / y
Less than or equal	<=	Nat -> Nat -> Bool	x <= y
Less than	<	Nat -> Nat -> Bool	x < y
Greater than or equal	>=	Nat -> Nat -> Bool	x >= y
Greater than	>	Nat -> Nat -> Bool	x >= y

Note that inequalities can be chained, so that x < y <= z will be expanded to x < y and y <= z.

Rationals

Rational numbers in Vehicle are stored using arbitrary precision. The type of rational numbers is written as Rat.

The available operations over rationals are:

Operation	Symbol	Type	Example
Addition	+	Rat -> Rat -> Rat	x + y
Subtraction	-	Rat -> Rat -> Rat	x - y
Multiplication	*	Rat -> Rat -> Rat	x * y
Division	/	Rat -> Rat -> Rat	x / y
Negation	-	Rat -> Rat	- y
Less than or equal	<=	Rat -> Rat -> Bool	x <= y
Less than	<	Rat -> Rat -> Bool	x < y
Greater than or equal	>=	Rat -> Rat -> Bool	x >= y
Greater than	>	Rat -> Rat -> Bool	x >= y

Note

We are aware that the disconnect between the semantics of rational/real numbers and floating point can lead to soundness bugs in verification. Adding floating point types with configurable precision is on our road map.