decode

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.decode

English

Decoding is primitive recursive, given Primcodable structure.

Русский

Декодирование примитивно-рекурсивно при наличии структуры Primcodable.

LaTeX

$$$$\\text{Primrec.decode}:\\; Primrec(\\decode)$$$$

Lean4

protected theorem decode : Primrec (@decode α _) :=
  Nat.Primrec.succ.comp (Primcodable.prim α)

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

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

Разделы

Аффилиация

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