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)