instance instLawfulOrderMax_projects {α : Type u_1} [ha : LinearOrder α] : Std.LawfulOrderMax α

def mkList {α : Type u_1} (n : ℕ) (f : ℕ → α) : List α

Equations

• mkList n f = List.map f (List.range n)

def List.init {α : Type u_4} : List α → List α

Equations

• [].init = []
• [head].init = []
• (x_1 :: ys).init = x_1 :: ys.init

def List.combinations {α : Type u_1} (xs : List α) (n : ℕ) : List (List α)

Equations

• xs.combinations n = sequence (List.replicate n xs)

def List.atMostOne : List Bool → Bool

Equations

• [].atMostOne = true
• (b :: bs).atMostOne = if b = true then !bs.or else bs.atMostOne

def List.mapWith {α : Type u_1} {β : Type u_2} (xs : List α) (f : (x : α) → x ∈ xs → β) : List β

Equations

• [].mapWith f_2 = []
• (x :: ys).mapWith f_2 = f_2 x ⋯ :: ys.mapWith fun (y : α) (h₁ : y ∈ ys) => f_2 y ⋯

noncomputable def List.dfltMapWith {α : Type u_1} {β : Type u_2} {xs : List α} (f : (x : α) → x ∈ xs → β) (h : xs ≠ []) : β

Equations

• List.dfltMapWith f_2 h_2 = ⋯.elim
• List.dfltMapWith f_2 h_2 = ⋯.some

def List.foldlWith {α : Type u_1} {β : Sort u_4} (xs : List α) (f : β → (x : α) → x ∈ xs → β) (z : β) : β

Equations

• [].foldlWith f_2 z = z
• (x :: ys).foldlWith f_2 z = ys.foldlWith (fun (acc : β) (y : α) (h₁ : y ∈ ys) => f_2 acc y ⋯) (f_2 z x ⋯)

def List.toSet {α : Type u_1} (xs : List α) : Set α

Equations

• xs.toSet = {x : α | x ∈ xs}

def List.toVec {α : Type u_1} (xs : List α) : Fin xs.length → α

Equations

• xs.toVec x✝ = xs[x✝]

def List.min!! {α : Type u_1} [Min α] [Top α] (xs : List α) : α

Equations

• xs.min!! = xs.min?.getD ⊤

def List.max!! {α : Type u_1} [Max α] [Bot α] (xs : List α) : α

Equations

• xs.max!! = xs.max?.getD ⊥