encodeList — Mathlib

English

An explicit encoding function for lists: the empty list encodes to 0, and a::l encodes to succ (pair (encode a) (encodeList l)).

Русский

Явная кодировка списка: пустой список кодируется как 0, a :: l кодируется как succ (pair (encode a) (encodeList l)).

LaTeX

$$$\\encodeList([]) = 0 \\quad\\wedge\\quad \\encodeList(a::l) = \\operatorname{succ}(\\operatorname{pair}(\\encode a)(\\encodeList l)).$$$

Lean4

/-- Explicit encoding function for `List α` -/
def encodeList : List α → ℕ
  | [] => 0
  | a :: l => succ (pair (encode a) (encodeList l))

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