With [[Dependent Typetype|dependent types]], it is possible for values to appear in the types; in effect, any value-level computation can be performed during typechecking. The following defines a type of lists of statically known length, traditionally called 'vectors':
