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	Syntax	Type	Support
Add	x + y	Nat → Nat → Nat
Multiply	x * y	Nat → Nat → Nat
Divide	x / y	Nat → Nat → Real
Compare	x < y x > y x <= y x >= y x == y x != y	Nat → Nat → Bool

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	Syntax	Type	Support
Add	x + y	Real → Real → Real
Subtract	x - y	Real → Real → Real
Multiply	x * y	Real → Real → Real	(⤴)
Divide	x / y	Real → Real → Real	(⤴)
Negation	- y	Real → Real
Compare	x < y x > y x <= y x >= y x == y x != y	Real → Real → Bool
Min	min x y	Real → Real → Real
Max	max x y	Real → Real → Real
Infinity	infinity	Real

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.