seq

Mathlib.Control.Functor

URI: https://scilib.ai/kg/mathlib#Functor.Comp.seq

Lean4

/-- The `<*>` operation for the composition of applicative functors. -/
protected def seq {α β : Type v} : Comp F G (α → β) → (Unit → Comp F G α) → Comp F G β
  | Comp.mk f, g =>
    match g () with
    | Comp.mk x => Comp.mk <| (· <*> ·) <$> f <*> x

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

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

Разделы

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

Аффилиация

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