This file contains a helper function that generates all possible lists over a given list of candidates such that each of the lists has a given length. Since the definition would hardly be useful in proofs, the accompanying theorem states the desired properties ensured by the definition.

def CustomBasicDatastructures.all_lists_of_length {α : Type u_1} (candidates : List α) : Nat → List (List α)

Equations

• One or more equations did not get rendered due to their size.
• CustomBasicDatastructures.all_lists_of_length candidates Nat.zero = [[]]

@[simp]

theorem CustomBasicDatastructures.mem_all_lists_of_length {α : Type u_1} (candidates : List α) (length : Nat) (as : List α) : as ∈ all_lists_of_length candidates length ↔ as.length = length ∧ ∀ (a : α), a ∈ as → a ∈ candidates