Definitions on lazy lists

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

@[deprecated "No deprecation message was provided." (since := "2024-07-22")]

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 "No deprecation message was provided." (since := "2024-07-22")]

instance LazyList.instTraversable : Traversable LazyList

Equations

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

@[deprecated "No deprecation message was provided." (since := "2024-07-22")]

instance LazyList.instLawfulTraversable : LawfulTraversable LazyList

@[simp, deprecated "No deprecation message was provided." (since := "2024-07-22")]

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

@[deprecated "No deprecation message was provided." (since := "2024-07-22")]

instance LazyList.instLawfulMonad_mathlib : LawfulMonad LazyList