destruct_ofSeq — Mathlib

English

The toList of the List-to-Stream encoding of l includes l as an element.

Русский

ToList от кодирования списка l в поток включает l как элемент.

LaTeX

$$$$\mathrm{toList}(\mathrm{ofList}\,l) \ni l.$$$$

Lean4

@[simp]
theorem destruct_ofSeq (s : Seq α) : destruct (ofSeq s) = Computation.pure (s.head.map fun a => (a, ofSeq s.tail)) :=
  destruct_eq_pure <|
    by
    simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap, Seq.head]
    rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
    rcases Seq.get? s 0 with - | a
    · rfl
    dsimp only [(· <$> ·)]
    simp

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