corec_cons — Mathlib

English

If f(b) = some(x,s), then corec f b = cons x (corec f s).

Русский

Если f(b) = some(x,s), то corec f b = cons x (corec f s).

LaTeX

$$$\\forall f\\ b\\ x\\ s, f(b) = \\text{Option}.some\\ (x, s) \\Rightarrow \\mathrm{corec} f b = \\mathrm{cons}\ x\\ (\\mathrm{corec} f\; s)$$$

Lean4

theorem corec_cons {f : β → Option (α × β)} {b : β} {x : α} {s : β} (h : f b = .some (x, s)) :
    corec f b = cons x (corec f s) := by
  apply destruct_eq_cons
  simp [h]

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