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	Syntax	Type	Support
Conjunction	x and y	Bool → Bool → Bool
Disjunction	x or y	Bool → Bool → Bool
Implication	x => y	Bool → Bool → Bool
Negation	not x	Bool → Bool
Conditional	if x then y else z	Bool → A → A → A

Conditionals

Conditional statements are written as follows:

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

In a functional language like Vehicle 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.

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

• 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