def Chapter12.parts₃ {α : Type} : List α → List (Partition α)

Equations

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

def Chapter12.ok (xs : List ℕ) : Bool

Equations

• Chapter12.ok xs = xs.all fun (x : ℕ) => decide (x > 0)

def Chapter12.okextendl (x : ℕ) : Partition ℕ → List (Partition ℕ)

Equations

• Chapter12.okextendl x = List.filter (Chapter12.ok ∘ List.head!) ∘ Chapter12.extendl x

def Chapter12.leftmin (xs : List ℕ) : Bool

Equations

• Chapter12.leftmin xs = xs.all fun (x : ℕ) => decide (xs.head! ≤ x)

def Chapter12.rightmax (xs : List ℕ) : Bool

Equations

• Chapter12.rightmax xs = xs.all fun (x : ℕ) => decide (x ≤ Chapter12.last xs)

def Chapter12.ordered (xs : List ℕ) : Bool

Equations

• Chapter12.ordered xs = (List.zipWith (fun (x1 x2 : ℕ) => decide (x1 ≤ x2)) xs xs.tail).and

def Chapter12.nmatch (xs : List ℕ) : Bool

Equations

• Chapter12.nmatch xs = (List.zipWith (fun (x1 x2 : ℕ) => decide (x1 ≠ x2)) xs (List.range xs.length)).and

def Chapter12.suffixClosed (p : List ℕ → Bool) : Prop

Equations

• Chapter12.suffixClosed p = ∀ (xs ys : List ℕ), p (xs ++ ys) = true → p ys = true

def Chapter12.prefixClosed (p : List ℕ → Bool) : Prop

Equations

• Chapter12.prefixClosed p = ∀ (xs ys : List ℕ), p (xs ++ ys) = true → p xs = true