corecOn

Mathlib.Data.Stream.Defs

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

Lean4

/-- Given an initial value `a : α` and functions `f : α → β` and `g : α → α`,
`corecOn a f g` creates a stream by repeatedly:
1. Applying `f` to the current value to get the next stream element
2. Applying `g` to get the next value to process
This is equivalent to `corec f g a`. -/
def corecOn (a : α) (f : α → β) (g : α → α) : Stream' β :=
  corec f g a

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

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

Разделы

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

Аффилиация

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