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} :
stream α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} :
state σ ασ → stream α

Use a state monad to generate a stream through corecursion

Equations