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 



Multiplication 



Division 



Less than or equal 



Less than 



Greater than or equal 



Greater than 



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 



Subtraction 



Multiplication 



Division 



Negation 



Less than or equal 



Less than 



Greater than or equal 



Greater than 



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.