Def stream.append_stream
Modification history
2021-11-26 07:20
src/data/stream/defs.lean
chore(data/stream): move most defs to a new file (#10458)
Modified stream.append_streamView on Github →2021-10-30 01:45
src/data/stream/init.lean
chore(*): update to Lean-3.35.0c (#9988) …
Added stream.append_streamView on Github →