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.
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.