English
toList' on a cons connection preserves the relation with think of cons.
Русский
toList' при конструировании через cons сохраняет отношение с think.
LaTeX
$$$$toList'(\,l, \mathrm{cons}\,a\,s) = \mathrm{think}\left(\mathrm{toList}'(a::l, s)\right).$$$$
Lean4
@[simp]
theorem toList'_cons (l : List α) (s : WSeq α) (a : α) :
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, cons a 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'))
(a :: l, s)).think :=
destruct_eq_think <| by simp [cons]
