English
Think commutes with toList': the think step on the corec is equal to applying think after toList.
Русский
Think коммутирует с toList': переход think на corec равен применению think после toList.
LaTeX
$$$$\mathrm{toList'\} (l, s).\mathrm{think} = \mathrm{corec}\, (\ldots)\ (l, s^{\mathrm{think}}).$$$$
Lean4
@[simp]
theorem toList'_think (l : List α) (s : WSeq α) :
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, think s) =
(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, s)).think :=
destruct_eq_think <| by simp [think]
