encodeNat

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.encodeNat

English

An encoding of natural numbers into lists of booleans is defined by encodeNat.

Русский

Задано кодирование натуральных чисел в список булевых значений через encodeNat.

LaTeX

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

Lean4

/-- An encoding function of ℕ in bool. -/
def encodeNat (n : ℕ) : List Bool :=
  encodeNum n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru