Type synonyms

Although Vehicle’s builtin types are sufficient to write a wide range of specifications, specifications can often be made more readable by using the type keyword to defining meaningful synonyms for those that are used repeatedly.

For example, when defining a robustness specification for the MNIST dataset which contains 24x24 greyscale images, in order to avoid having to repeatedly write Tensor Rat [24, 24], one could declare Image as a synonym for it and use it as follows:

type Image = Tensor Rat [24, 24]

classify : Image -> Tensor Rat [10]

trainingDataset : List Image

robustAround : Image -> Bool
robustAround x = ...