def Chapter7.minimumBy {α : Type} (cmp : α → α → Ordering) : List α → Option α

Equations

• Chapter7.minimumBy cmp [] = none
• Chapter7.minimumBy cmp (x_1 :: xs) = some (List.foldr (fun (y r : α) => bif decide (cmp y r = Ordering.lt) then y else r) x_1 xs)

def Chapter7.minWith₁ {α β : Type} [Ord β] (f : α → β) (xs : List α) : Option α

Equations

• Chapter7.minWith₁ f xs = Chapter7.minimumBy (fun (x y : α) => compare (f x) (f y)) xs

def Chapter7.minWith₂ {α β : Type} [Ord β] (f : α → β) (xs : List α) : Option α

Equations

• Chapter7.minWith₂ f xs = do let pair ← Chapter7.minimumBy (fun (x y : β × α) => compare x.1 y.1) (List.map (fun (x : α) => (f x, x)) xs) some pair.2

instance Chapter7.instOrdFloat_fad : Ord Float

Equations

• Chapter7.instOrdFloat_fad = { compare := fun (x y : Float) => if x < y then Ordering.lt else if (x == y) = true then Ordering.eq else Ordering.gt }

def Chapter7.minsWith {α β : Type} [Ord β] (f : α → β) (xs : List α) : List α

Equations

• One or more equations did not get rendered due to their size.

def Chapter7.minsWith' {α β : Type} [Ord β] (f : α → β) (xs : List α) : List α

Equations

• One or more equations did not get rendered due to their size.

def Chapter7.minsWith'.tuple {α β : Type} (f : α → β) (x : α) : β × α

Equations

• Chapter7.minsWith'.tuple f x = (f x, x)

@[irreducible]

def Chapter7.interleave {α : Type} : List α → List α → List (List α)

Equations

• One or more equations did not get rendered due to their size.
• Chapter7.interleave x✝ [] = [x✝]
• Chapter7.interleave [] x✝ = [x✝]

def Chapter7.cp {α β : Type} (xs : List α) (ys : List β) : List (α × β)

Equations

• Chapter7.cp xs ys = Chapter1.concatMap (fun (x : α) => List.map (fun (y : β) => (x, y)) ys) xs

def Chapter7.perms₁ {α : Type} : List α → List (List α)

Equations

• One or more equations did not get rendered due to their size.
• Chapter7.perms₁ [] = [[]]
• Chapter7.perms₁ [x_1] = [[x_1]]

def Chapter7.min_list_list : List ℕ → List ℕ → List ℕ

Equations

• Chapter7.min_list_list [] x✝ = []
• Chapter7.min_list_list x✝ [] = []
• Chapter7.min_list_list (a :: as) (b :: bs) = if a < b then a :: as else if a > b then b :: bs else a :: Chapter7.min_list_list as bs

instance Chapter7.instMinListNat_fad : Min (List ℕ)

Equations

• Chapter7.instMinListNat_fad = { min := Chapter7.min_list_list }

def Chapter7.pick₂ : List ℕ → Option (ℕ × List ℕ)

Equations

• Chapter7.pick₂ [] = none
• Chapter7.pick₂ [x_1] = some (x_1, [])
• Chapter7.pick₂ (x_1 :: xs) = match Chapter7.pick₂ xs with | none => none | some (y, ys) => if x_1 ≤ y then some (x_1, xs) else some (y, x_1 :: ys)

def Chapter7.S73.mktuples' : List Denom → ℕ → List Tuple

Equations

• Chapter7.S73.mktuples' [1] x✝ = [[x✝]]
• Chapter7.S73.mktuples' [] x✝ = panicWithPosWithDecl "Fad.«Chapter7-Ex»" "Chapter7.S73.mktuples'" 160 18 "mktuples: invalid empty list"
• Chapter7.S73.mktuples' (d :: ds) x✝ = List.flatMap (fun (c : ℕ) => List.map (fun (cs : List ℕ) => c :: cs) (Chapter7.mktuples₀ ds (x✝ - c * d))) (List.range (x✝ / d + 1))

def Chapter7.S73.mkchange' (ds : List Denom) : ℕ → Tuple

Equations

• Chapter7.S73.mkchange' ds = Chapter7.minWith List.sum ∘ Chapter7.S73.mktuples' ds

def Chapter7.S73.urds : List ℕ

Equations

• Chapter7.S73.urds = [100, 50, 20, 15, 5, 2, 1]