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 -> Real	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
Min	min	Nat -> Nat -> Bool	min x y
Max	max	Nat -> Nat -> Bool	max x y

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

Reals

The type of real numbers is written as Real.

The available operations over reals are:

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

Note

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