cAdd

Mathlib.Data.Num.Bitwise

URI: https://scilib.ai/kg/mathlib#SNum.cAdd

Lean4

/-- `SNum.cAdd n m a` is `n + m + a` (where `a` should be read as either 0 or 1).
`a` represents a carry bit. -/
def cAdd : SNum → SNum → Bool → SNum :=
  rec' (fun a p c ↦ czAdd c a p) fun a p IH ↦
    rec' (fun b c ↦ czAdd c b (a :: p)) fun b q _ c ↦ Bool.xor3 a b c :: IH q (Bool.carry a b c)

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

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

Разделы

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

Аффилиация

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