# 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

`+`

`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

`+`

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