mathlib documentation

data.stream.basic

Additional instances and attributes for streams #

@[instance]
def stream.inhabited {α : Type u_1} [inhabited α] :
Equations
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
theorem stream.length_take {α : Type u_1} (s : stream α) (n : ) :
(s.take n).length = n
def stream.corec_state {σ α : Type u_1} (cmd : state σ α) (s : σ) :

Use a state monad to generate a stream through corecursion

Equations