# Logic

## Booleans

Like many languages, Vehicle has booleans. The type of boolean values is `Bool`, and there are two values `True` and `False`.

The available operations over booleans are:

Operation

Symbol

Type

Example

Conjunction

`and`

`Bool -> Bool -> Bool`

`x and y`

Disjunction

`or`

`Bool -> Bool -> Bool`

`x or y`

Implication

`=>`

`Bool -> Bool -> Bool`

`x => y`

Negation

`not`

`Bool -> Bool`

`not x`

## Conditionals

Conditional statements are written using the syntax `if .. then .. else ..` and have type `Bool -> A -> A -> A` for any type `A`. For example:

```if f x > 0 then x < 0 else x > 0
```

In a functional language like Vehicle (and unlike in imperative languages) all statements must return a value. Therefore it is not possible to omit the `else` branch when writing a conditional.

Note

As discussed in the Tips and Tricks section, `if then else` should be used sparingly, as each conditional in the final normalised expression approximately doubles the time taken to verify the specification.

Note

Due to decidability and query dependency issues, the condition of an `if then else` statement may not contain a quantification over a variable with an infinite domain. For example, the following is not allowed:

```if (forall (x : Rat) . f x > 0) then 2 else 3
```

## Equality

Two expressions of the same type can be tested for equality/inequality using the `==` and `!=` operators respectively.

The type of these operators are `A -> A -> Bool` where `A` can be any of the following types:

• `Bool`, `Nat`, `Int`, `Rat`.

• `Index d` for any value of `d`.

• `List A` if type `A` also supports the operators.

• `Vector A n` if type `A` also supports the operators.

• `Tensor A dims` if type `A` also supports the operators.

For example:

```forall x . x != 0 => f x == 1
```