aux

Mathlib.Data.WSeq.Basic

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

Lean4

/-- auxiliary definition of `destruct_join` over weak sequences -/
@[simp]
def aux : Option (WSeq α × WSeq (WSeq α)) → Computation (Option (α × WSeq α))
  | none => Computation.pure none
  | some (s, S) => (destruct (append s (join S))).think

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

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

Разделы

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

Аффилиация

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