Definitions on lazy lists

This file is entirely deprecated, and contains various definitions and proofs on lazy lists.

@[deprecated]

def LazyList.listEquivLazyList (α : Type u_1) : List α ≃ LazyList α

Isomorphism between strict and lazy lists.

Equations

• LazyList.listEquivLazyList α = { toFun := LazyList.ofList, invFun := LazyList.toList, left_inv := ⋯, right_inv := ⋯ }

@[deprecated]

instance LazyList.instTraversable : Traversable LazyList

Equations

• LazyList.instTraversable = Traversable.mk @LazyList.traverse

@[deprecated]

instance LazyList.instLawfulTraversable : LawfulTraversable LazyList

Equations

• LazyList.instLawfulTraversable = ⋯

@[simp, deprecated]

theorem LazyList.bind_singleton {α : Type u_1} (x : LazyList α) : x.bind LazyList.singleton = x

@[deprecated]

instance LazyList.instLawfulMonad_mathlib : LawfulMonad LazyList

Equations

• LazyList.instLawfulMonad_mathlib = ⋯