encode

Mathlib.Computability.Primrec

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

English

Encoding maps preserve Primrec structure via equivalences of primcodable types.

Русский

Кодирование сохраняет примитивно-рекурсивную структуру через эквиваленции типов Primcodable.

LaTeX

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

Lean4

protected theorem encode : Primrec (@encode α _) :=
  (Primcodable.prim α).of_eq fun n => by cases @decode α _ n <;> rfl

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

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

Разделы

Аффилиация

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