f — Mathlib · SciLib

English

Corecursor constructor for corec: defines a function f to produce Computation α from β.

Русский

Конструктор ядрового курсора для corec задаёт функцию f: β → α ⊕ β, которая порождает вычисление.

LaTeX

$$$\\mathrm{corec} : (\\beta \\to \\alpha \\oplus \\beta) \\to \\beta \\to \\mathrm{Computation}\\,\\alpha$$$

Lean4

/-- Corecursor constructor for `corec` -/
def f (f : β → α ⊕ β) : α ⊕ β → Option α × (α ⊕ β)
  | Sum.inl a => (some a, Sum.inl a)
  | Sum.inr b =>
    (match f b with
      | Sum.inl a => some a
      | Sum.inr _ => none,
      f b)

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