unaryEncodeNat — Mathlib

English

A unary encoding function of ℕ in bool is defined, mapping n to a list of n true's preceded recursively by true's.

Русский

Определена унарная кодировка ℕ в булевы значения, отправляющая n в список из n истинных значений.

LaTeX

$$$ \mathrm{unaryEncodeNat} : \mathbb{N} \to \mathrm{List}\,\mathrm{Bool} $$$

Lean4

/-- A unary encoding function of ℕ in bool. -/
def unaryEncodeNat : Nat → List Bool
  | 0 => []
  | n + 1 => true :: unaryEncodeNat n

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