optionToList

Mathlib.Computability.Primrec

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

← MathLib Explorer

English

Option.toList is primitive recursive.

Русский

Option.toList примитивно вычислима.

LaTeX

$$$\\mathrm{Primrec}(\\mathrm{Option}.\\mathrm{toList})$$$

Lean4

theorem optionToList : Primrec (Option.toList : Option α → List α) :=
  (option_casesOn Primrec.id (const []) ((list_cons.comp Primrec.id (const [])).comp₂ Primrec₂.right)).of_eq
    (fun o => by rcases o <;> simp)

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

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

Разделы

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

Аффилиация

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