toList'_nil — Mathlib

English

toList' on a nil tail yields pure reverse of the list.

Русский

toList' для nil даёт pure обратный порядок списка.

LaTeX

$$$$toList'\, (l, \\\mathrm{nil}) = \mathrm{pure}\, l^{\mathrm{reverse}}.$$$$

Lean4

@[simp]
theorem toList'_nil (l : List α) :
    Computation.corec
        (fun ⟨l, s⟩ =>
          match Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
        (l, nil) =
      Computation.pure l.reverse :=
  destruct_eq_pure rfl

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