primrec₂_curry

Mathlib.Computability.PartrecCode

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.primrec₂_curry

← MathLib Explorer

English

The two-argument primitive recursive function curry is primitive recursive.

Русский

Функция curry с двумя аргументами является примитивно вычислимой.

LaTeX

$$$\\mathrm{Primrec}_2\\; \\text{curry}$$$

Lean4

theorem primrec₂_curry : Primrec₂ curry :=
  primrec₂_comp.comp Primrec.fst <| primrec₂_pair.comp (primrec_const.comp Primrec.snd) (_root_.Primrec.const Code.id)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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