bind_pure'

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.bind_pure'

English

bind s pure = s.

Русский

bind s pure = s.

LaTeX

$$$$ \operatorname{bind} s \mathrm{pure} = s. $$$$

Lean4

@[simp]
theorem bind_pure' (s : Computation α) : bind s pure = s := by simpa using bind_pure id s

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

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

Разделы

Аффилиация

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