ofAscListAux₂ — Mathlib

English

Auxiliary definition for ofAscList, further processing of ascending lists into Ordnode.

Русский

Дальнейшее вспомогательное определение для преобразования возрастающих списков в Ordnode.

LaTeX

$$$$ \mathrm{ofAscListAux_2}: \ List\; \alpha \to \ Ordnode\; \alpha \to \mathbb{N} \to \ Ordnode\; \alpha $$$$

Lean4

/-- Auxiliary definition for `ofAscList`. -/
def ofAscListAux₂ : List α → Ordnode α → ℕ → Ordnode α
  | [] => fun t _ => t
  | x :: xs => fun l s =>
    match ofAscListAux₁ xs s with
    | (r, ⟨ys, h⟩) =>
      have := Nat.lt_succ_of_le h
      ofAscListAux₂ ys (link l x r) (s <<< 1)
termination_by l => l.length

Похожие утверждения