add

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Nat.Primrec'.add

← MathLib Explorer

English

Addition of two natural numbers is Primrec'.

Русский

Сложение двух натуральных чисел является Primrec'.

LaTeX

$$$\mathrm{add} : \ Primrec'\ 2\ (fun\ v => v.head + v.tail.head)$$$

Lean4

theorem add : @Primrec' 2 fun v => v.head + v.tail.head :=
  (prec head (succ.comp₁ _ (tail head))).of_eq fun v => by simp; induction v.head <;> simp [*, Nat.succ_add]

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

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

Разделы

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

Аффилиация

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