### Abstract

This theory introduces a type constructor for lists with known length, also known as "vectors". Those vectors are indexed with a numeral type that represent their length. This can be employed to avoid carrying around length constraints on lists. Instead, those constraints are discharged by the type checker. As compared to the vectors defined in the distribution, this definition can easily work with unit vectors. We exploit the fact that the cardinality of an infinite type is defined to be 0: thus any infinite length index type represents a unit vector. Furthermore, we set up automation and BNF support.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Fixed_Length_Vector

- Fixed_Length_Vector

## Cite

×

Fixed_Length_Vector-AFP

    @article{Fixed_Length_Vector-AFP,
      author  = {Lars Hupel},
      title   = {Fixed-length vectors},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Fixed_Length_Vector.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Aug 20, 2023 : Isabelle2022