cycleF

Mathlib.Data.Stream.Defs

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

English

cycleF returns the current value from the cycle state, i.e., the first component of the tuple.

Русский

cycleF возвращает текущее значение цикла, то есть первый элемент пары.

LaTeX

$$$ \text{cycleF}(v, L, v', L') = v. $$$

Lean4

/-- An auxiliary definition for `Stream'.cycle` corecursive def -/
protected def cycleF : α × List α × α × List α → α
  | (v, _, _, _) => v

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

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

Разделы

Аффилиация

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