trList — Mathlib

English

Lists are translated into a sequence by translating elements via trNat and appending a cons symbol between elements.

Русский

Списки переводятся последовательностью: каждый элемент кодируется через trNat, затем между элементами добавляется конc.

LaTeX

$$$\\operatorname{trList}(L) = \\{\\text{translation of }L\\}$$$

Lean4

/-- Lists are translated with a `cons` after each encoded number.
For example:

    [] = []
    [0] = [cons]
    [1] = [bit1, cons]
    [6, 0] = [bit0, bit1, bit1, cons, cons]
-/
@[simp]
def trList : List ℕ → List Γ'
  | [] => []
  | n :: ns => trNat n ++ Γ'.cons :: trList ns

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