head_cons

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.head_cons

English

The head of a cons cell yields the just the head as a pure some.

Русский

Голова конструкторa cons даёт pure some(a).

LaTeX

$$$$\mathrm{head}(\mathrm{cons}(a,s))=\mathrm{pure}(\mathrm{some}(a)).$$$$

Lean4

@[simp]
theorem head_cons (a : α) (s) : head (cons a s) = Computation.pure (some a) := by simp [head]

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

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

Разделы

Аффилиация

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