option_some

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Computable.option_some

English

The constructor Option.some: α → Option α is computable.

Русский

Конструктор Some: α → Option α вычислимо.

LaTeX

$$$\mathrm{Option}.some: \alpha \to \mathrm{Option}\,\alpha$ is computable.$$

Lean4

theorem option_some : Computable (@Option.some α) :=
  Primrec.option_some.to_comp

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

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

Разделы

Аффилиация

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