Lists
Basics
Lists are collections of an arbitrary number of elements of a single type.
The type of a list of elements of type A
is written as List A
, e.g.
List Nat
is a list of natural numbers.
Lists can be created using the [x_1, ..., x_n]
syntax, e.g. [5, 2, 6]
.
Operations
The following operations over lists are currently supported:
Operation |
Symbol |
Type |
Example |
---|---|---|---|
Map |
|
|
|
Fold |
|
|
|
Absence of a lookup function
It is a deliberate design decision that there is no operation to lookup the element at a given position in a list. Therefore, the individual elements of a list can only be accessed by quantifying over them, e.g.
myList : List Rat
myList = [1, 1, 2, 3, 5, 8]
positive : Bool
positive = forall x in myList . x >= 0
This is because every Vehicle specification is a mathematical formula, and in
order to maintain this relationship we need to guarantee the absence of
out-of-bounds errors.
If you really need to look up the value at an arbitrary index then you should be
using a Vector
instead of a List
.