results_pure

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.results_pure

English

In the Computation monad, for any a, the results of pure a are exactly a and a trace length 0.

Русский

В монаде Computation результаты чистого значения a равны a и длина трассы равна 0.

LaTeX

$$$\\text{Results}(\\text{pure } a)\; a\\;0.$$$

Lean4

theorem results_pure (a : α) : Results (pure a) a 0 :=
  ⟨ret_mem a, length_pure _⟩

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

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

Разделы

Аффилиация

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