Lean4
/-- `union s1 s2` is a weak sequence which interleaves `s1` and `s2` in
some order (nondeterministically). -/
def union (s1 s2 : WSeq α) : WSeq α :=
@Seq.corec (Option α) (WSeq α × WSeq α)
(fun ⟨s1, s2⟩ =>
match Seq.destruct s1, Seq.destruct s2 with
| none, none => none
| some (a1, s1'), none => some (a1, s1', nil)
| none, some (a2, s2') => some (a2, nil, s2')
| some (none, s1'), some (none, s2') => some (none, s1', s2')
| some (some a1, s1'), some (none, s2') => some (some a1, s1', s2')
| some (none, s1'), some (some a2, s2') => some (some a2, s1', s2')
| some (some a1, s1'), some (some a2, s2') => some (some a1, cons a2 s1', s2'))
(s1, s2)
