def Chapter7.NonEmptyList (α : Type) : Type

Equations

• Chapter7.NonEmptyList α = { l : List α // l.length > 0 }

@[irreducible]

def Chapter7.foldr1₀ {a : Type} (f : a → a → a) (as : NonEmptyList a) : a

Equations

• Chapter7.foldr1₀ f as = if h₂ : (↑as).length = 1 then (↑as).head ⋯ else let as' := (↑as).tail; have this := ⋯; f ((↑as).head ⋯) (Chapter7.foldr1₀ f ⟨as', ⋯⟩)

@[irreducible]

def Chapter7.foldr1₁ {a : Type} (f : a → a → a) (as : List a) (h : as.length > 0 := by decide) : a

Equations

• Chapter7.foldr1₁ f as h = if h₂ : as.length = 1 then as.head ⋯ else f (as.head ⋯) (Chapter7.foldr1₁ f as.tail ⋯)

def Chapter7.foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a

Equations

• Chapter7.foldr1 f [] = default
• Chapter7.foldr1 f (x_1 :: xs) = List.foldr f x_1 xs

def Chapter7.minWith {a b : Type} [LE b] [Inhabited a] [DecidableRel fun (x1 x2 : b) => x1 ≤ x2] (f : a → b) (as : List a) : a

Equations

• Chapter7.minWith f as = Chapter7.foldr1 ((fun (f : a → b) (x y : a) => bif decide (f x ≤ f y) then x else y) f) as

def Chapter7.pairs {a : Type} (xs : List a) : List (a × a)

Equations

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

def Chapter7.ic {a : Type} [LT a] [h₁ : DecidableRel fun (x1 x2 : a) => x1 < x2] (xs : List a) : ℕ

Equations

• Chapter7.ic xs = (List.filter (fun (p : a × a) => decide (p.1 > p.2)) (Chapter7.pairs xs)).length

def Chapter7.extend {a : Type} : a → List a → List (List a)

Equations

• Chapter7.extend x✝ [] = [[x✝]]
• Chapter7.extend x✝ (y :: xs) = (x✝ :: y :: xs) :: List.map (fun (x : List a) => y :: x) (Chapter7.extend x✝ xs)

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

Equations

• Chapter7.perms = List.foldr (Chapter1.concatMap ∘ Chapter7.extend) [[]]

def Chapter7.sort {a : Type} [LT a] [h₁ : DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• Chapter7.sort = Chapter7.minWith Chapter7.ic ∘ Chapter7.perms

def Chapter7.gstep {a : Type} [LT a] [h₁ : DecidableRel fun (x1 x2 : a) => x1 < x2] (x : a) : List a → List a

Equations

• Chapter7.gstep x = Chapter7.minWith Chapter7.ic ∘ Chapter7.extend x

def Chapter7.picks {a : Type} (xs : List a) : List (a × List a)

Equations

• Chapter7.picks [] = []
• Chapter7.picks (x_1 :: xs_1) = (x_1, xs_1) :: Chapter7.picks.helper x_1 (Chapter7.picks xs_1)

def Chapter7.picks.helper {a : Type} : a → List (a × List a) → List (a × List a)

Equations

• Chapter7.picks.helper x✝ [] = []
• Chapter7.picks.helper x✝ ((y, ys) :: rest) = (y, x✝ :: ys) :: Chapter7.picks.helper x✝ rest

def Chapter7.pick {a : Type} [Inhabited a] [LE a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : a × List a

Equations

• Chapter7.pick xs = match Chapter7.picks xs with | [] => (default, []) | [p] => p | p :: ps => Chapter7.pick.aux p ps

def Chapter7.pick.aux {a : Type} [LE a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : a × List a → List (a × List a) → a × List a

Equations

• Chapter7.pick.aux (x_2, xs) [] = (x_2, xs)
• Chapter7.pick.aux (x_2, xs) ((y, ys) :: rest) = if x_2 ≤ y then Chapter7.pick.aux (x_2, xs) rest else Chapter7.pick.aux (y, ys) rest

instance Chapter7.instMinProdList_fad {a : Type} [Ord a] : Min (a × List a)

Equations

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

def Chapter7.pick₁ {a : Type} [Inhabited a] [Ord a] (xs : List a) : a × List a

Equations

• Chapter7.pick₁ xs = Chapter6.minimum (Chapter7.picks xs)

def Chapter7.sort₁ {a : Type} [Inhabited a] [Ord a] [LT a] [h₁ : DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• Chapter7.sort₁ [] = []
• Chapter7.sort₁ x✝ = match Chapter7.pick₁ x✝ with | (x, ys) => x :: Chapter7.sort ys

def Chapter7.sort₂ {a : Type} [Inhabited a] [LT a] [h₁ : DecidableRel fun (x1 x2 : a) => x1 < x2] [LE a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List a

Equations

• Chapter7.sort₂ [] = []
• Chapter7.sort₂ x✝ = match Chapter7.pick x✝ with | (x, ys) => x :: Chapter7.sort ys

@[reducible, inline]

abbrev Chapter7.Denom : Type

Equations

• Chapter7.Denom = ℕ

@[reducible, inline]

abbrev Chapter7.Tuple : Type

Equations

• Chapter7.Tuple = List ℕ

instance Chapter7.instMaxTuple : Max Tuple

Equations

• Chapter7.instMaxTuple = { max := fun (x y : Chapter7.Tuple) => if x > y then x else y }

def Chapter7.usds : List Denom

Equations

• Chapter7.usds = [100, 50, 25, 10, 5, 1]

def Chapter7.ukds : List Denom

Equations

• Chapter7.ukds = [200, 100, 50, 20, 10, 5, 2, 1]

def Chapter7.amount (ds : List Denom) (cs : Tuple) : ℕ

Equations

• Chapter7.amount ds cs = (List.zipWith (fun (x1 x2 : ℕ) => x1 * x2) ds cs).sum

def Chapter7.mktuples₀ : List Denom → ℕ → List Tuple

Equations

• Chapter7.mktuples₀ [1] x✝ = [[x✝]]
• Chapter7.mktuples₀ [] x✝ = panicWithPosWithDecl "Fad.Chapter7" "Chapter7.mktuples₀" 178 18 "mktuples: invalid empty list"
• Chapter7.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.mkchange₀ (ds : List Denom) : ℕ → Tuple

Equations

• Chapter7.mkchange₀ ds = Chapter7.minWith List.sum ∘ Chapter7.mktuples₀ ds

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

Equations

• Chapter7.mkchange₁ ds = Chapter6.maximum ∘ Chapter7.mktuples₀ ds

partial def Chapter7.mktuples₁ : List Denom → ℕ → List Tuple

def Chapter7.mkchange : List Denom → ℕ → Tuple

Equations

• Chapter7.mkchange [1] x✝ = [x✝]
• Chapter7.mkchange [] x✝ = panicWithPosWithDecl "Fad.Chapter7" "Chapter7.mkchange" 208 18 "mkchange: invalid empty list"
• Chapter7.mkchange (d :: ds) x✝ = x✝ / d :: Chapter7.mkchange ds (x✝ - x✝ / d * d)