recOn

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.recOn

Lean4

/-- Recursion principle for computations, compare with `List.recOn`. -/
@[elab_as_elim]
def recOn {motive : Computation α → Sort v} (s : Computation α) (pure : ∀ a, motive (pure a))
    (think : ∀ s, motive (think s)) : motive s :=
  match H : destruct s with
  | Sum.inl v => by
    rw [destruct_eq_pure H]
    apply pure
  | Sum.inr v =>
    match v with
    | ⟨a, s'⟩ => by
      rw [destruct_eq_think H]
      apply think

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

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

Разделы

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

Аффилиация

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