Commit 2023-03-29 02:46 a7e36e48
View on Github →refactor(data/seq): scope seq and wseq to namespace stream (#18284)
Adds namespace stream
to seq
and wseq
to ease the Mathlib4 port (as Seq
now name clashes with class Seq
(has_seq
in Lean 3).
This requires disambiguation between stream
and computation
where lemmas in each namespace have the same name, and requires explicit scoping to mathlib files that reference seq
and wseq
(often by open stream.seq as seq
)