Commit 2022-12-02 15:15 2aba5647

View on Github →

feat: port Data.Stream.Defs (#665) Mathlib SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 Diff view: https://github.com/leanprover-community/mathlib4/compare/7f9d342...stream

Estimated changes

added def Stream'.All
added def Stream'.Any
added def Stream'.apply
added def Stream'.cons
added def Stream'.const
added def Stream'.corec'
added def Stream'.corec
added def Stream'.corecOn
added def Stream'.cycle
added def Stream'.drop
added def Stream'.enum
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'