Theorems · Definition · logic and foundations

Computation.recOn

{α : Type u} →
  {motive : Computation α → Sort v} →
    (s : Computation α) → ((a : α) → motive (Computation.pure a)) → ((s : Computation α) → motive s.think) → motive s

Recursion principle for computations, compare with List.recOn.

Defined in

Mathlib.Data.Seq.Computation

Cited by

11 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound