Lists
Content created by Victor Blanchi, Egbert Rijke, Fredrik Bakke and Louis Wasserman.
Created on 2023-04-08.
Last modified on 2025-05-14.
Modules in the lists namespace
module lists where open import lists.arrays public open import lists.concatenation-lists public open import lists.equivalence-tuples-finite-sequences public open import lists.finite-sequences public open import lists.flattening-lists public open import lists.functoriality-finite-sequences public open import lists.functoriality-lists public open import lists.functoriality-tuples public open import lists.functoriality-tuples-finite-sequences public open import lists.lists public open import lists.lists-discrete-types public open import lists.permutation-lists public open import lists.permutation-tuples public open import lists.predicates-on-lists public open import lists.quicksort-lists public open import lists.reversing-lists public open import lists.sort-by-insertion-lists public open import lists.sort-by-insertion-tuples public open import lists.sorted-lists public open import lists.sorted-tuples public open import lists.sorting-algorithms-lists public open import lists.sorting-algorithms-tuples public open import lists.tuples public open import lists.universal-property-lists-wild-monoids public
Recent changes
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
- 2023-05-22. Victor Blanchi and Fredrik Bakke. Cycle prime decomposition is closed under cartesian product (#624).
- 2023-05-10. Victor Blanchi. Fundamental theorem of arithmetic (#612).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).