trNat — Mathlib

English

Binary encoding of natural numbers is reflected by the translation functions trNat and trNum, which are compatible via casting.

Русский

Двоичное кодирование чисел реализуется функциями перевода trNat и trNum, совместимыми через приведение типов.

LaTeX

$$$\\operatorname{trNat}(n) = \\operatorname{trNum}(n\\text{ cast})$$$

Lean4

/-- Because we use binary encoding, we define `trNat` in terms of `trNum`, using `Num`, which are
binary natural numbers. (We could also use `Nat.binaryRecOn`, but `Num` and `PosNum` make for
easy inductions.) -/
def trNat (n : ℕ) : List Γ' :=
  trNum n

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