mathlib documentation

data.stream.basic

Additional instances and attributes for streams #

source
@[protected, instance]
def stream.inhabited {α : Type u_1} [inhabited α] :
inhabited (stream α)
Equations
source
def stream.take {α : Type u_1} (s : stream α) (n : ℕ) :
list α

take s n returns a list of the n first elements of stream s

Equations
source
theorem stream.length_take {α : Type u_1} (s : stream α) (n : ℕ) :
(s.take n).length = n
source
def stream.corec_state {σ α : Type u_1} (cmd : state σ α) (s : σ) :
stream α

Use a state monad to generate a stream through corecursion

Equations