zipRight'_cons_cons — Mathlib

English

For any f, a, as, b, bs, zipRight' (a :: as) (b :: bs) = let r := zipRight' as bs in ( (Some a, b) :: r.fst, r.snd ).

Русский

Для любого f, a, as, b, bs: zipRight'(a :: as) (b :: bs) = let r := zipRight' as bs in ((Some a, b) :: r.fst, r.snd).

LaTeX

$$$\\forall a:\\alpha,\\ \\forall as:\\text{List }\\alpha,\\ \\forall b:\\beta,\\ \\forall bs:\\text{List }\\beta,\\ \\mathrm{zipRight}'\\ (a::as)\\ (b::bs) =\\ let\\ r := \\mathrm{zipRight}'\\ as\\ bs\\ in\\ ((\\mathrm{Some}\\ a, b) :: r.fst, r.snd)$$$

Lean4

@[simp]
theorem zipRight'_cons_cons :
    zipRight' (a :: as) (b :: bs) =
      let r := zipRight' as bs
      ((some a, b) :: r.fst, r.snd) :=
  rfl

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