destruct — Mathlib

English

destruct c returns either a value a or the rest of the computation tail.

Русский

destruct c возвращает либо значение a, либо остаток вычисления tail.

LaTeX

$$$\\text{destruct}(c) : \\alpha \\;\\oplus\\; \\text{Computation}(\\alpha)$$$

Lean4

/-- `destruct c` is the destructor for `Computation α` as a coinductive type.
  It returns `inl a` if `c = pure a` and `inr c'` if `c = think c'`. -/
def destruct (c : Computation α) : α ⊕ (Computation α) :=
  match c.1 0 with
  | none => Sum.inr (tail c)
  | some a => Sum.inl a

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