mathlib documentation

Additional instances and attributes for streams #

def stream.inhabited {α : Type u_1} [inhabited α] :
def stream.take {α : Type u_1} (s : stream α) (n : ) :
list α

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

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