list_flatten

Mathlib.Computability.Primrec

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

← MathLib Explorer

English

Flattening a list of lists is primitive recursive.

Русский

Сглаживание списка списков (flatten) примитивно вычислимо.

LaTeX

$$$\\mathrm{Primrec}\\left( \\mathrm{List}.\\mathrm{flatten} \\right)$$$

Lean4

theorem list_flatten : Primrec (@List.flatten α) :=
  (list_foldr .id (const []) <| to₂ <| comp (@list_append α _) snd).of_eq fun l => by dsimp; induction l <;> simp [*]

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

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

Разделы

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

Аффилиация

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