mathlib3
a7e36e48 - refactor(data/seq): scope seq and wseq to namespace stream (#18284)

Commit
2 years ago
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`) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading