Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-26 07:20 757aa6f8

View on Github →

chore(data/stream): move most defs to a new file (#10458)

Estimated changes

deleted def stream.take
added def stream.all
added def stream.any
added def stream.apply
added def stream.approx
added def stream.cons
added def stream.const
added def stream.corec'
added def stream.corec
added def stream.corec_on
added def stream.cycle
added def stream.drop
added def stream.even
added def stream.head
added def stream.inits
added def stream.iterate
added def stream.map
added def stream.nats
added def stream.nth
added def stream.odd
added def stream.pure
added def stream.tail
added def stream.tails
added def stream.take
added def stream.unfolds
added def stream.zip
added def stream
deleted def stream.all
deleted def stream.any
deleted def stream.apply
deleted def stream.approx
deleted def stream.cons
deleted def stream.const
deleted def stream.corec'
deleted def stream.corec
deleted def stream.corec_on
deleted def stream.cycle
deleted def stream.drop
deleted def stream.even
deleted def stream.head
deleted def stream.inits
deleted def stream.inits_core
deleted def stream.interleave
deleted def stream.iterate
deleted def stream.map
deleted def stream.nats
deleted def stream.nth
deleted def stream.odd
deleted def stream.pure
deleted def stream.tail
deleted def stream.tails
deleted def stream.unfolds
deleted def stream.zip
deleted def stream