Lists

Content created by Fredrik Bakke, Victor Blanchi, Egbert Rijke, Louis Wasserman and Šimon Brandner.

Created on 2023-04-08.
Last modified on 2025-09-12.

Modules in the lists namespace

module lists where

open import lists.arrays public
open import lists.concatenation-lists public
open import lists.concatenation-tuples public
open import lists.dependent-sequences 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.partial-sequences 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.repetitions-sequences public
open import lists.reversing-lists public
open import lists.sequences public
open import lists.shifting-sequences 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.subsequences public
open import lists.tuples public
open import lists.universal-property-lists-wild-monoids public

Recent changes

• 2025-09-12. Šimon Brandner. Add linear combinations, linear spans and tuple concatenation (#1537).
• 2025-08-30. Louis Wasserman and Fredrik Bakke. Move sequences to lists namespace (#1476).
• 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).