chore: deprecate LazyList (#884)

Batteries/Data/LazyList.lean

@@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Simon Hudon
 -/
 import Batteries.Data.Thunk
-
 /-!
 # Lazy lists
 
+Deprecated. This module is deprecated and will be removed in the future.
+Most use cases can use `MLList`. Without custom support from the kernel
+(previously provided in Lean 3) this type is not very useful,
+but was ported from Lean 3 anyway.
+
 The type `LazyList α` is a lazy list with elements of type `α`.
 In the VM, these are potentially infinite lists
 where all elements after the first are computed on-demand.
@@ -18,13 +22,15 @@ logically we can prove that `LazyList α` is isomorphic to `List α`.)
 /-- Lazy list.
 All elements (except the first) are computed lazily.
 -/
+@[deprecated "Consider using `MLList`." (since := "2024-07-15")]
 inductive LazyList (α : Type u) : Type u
   /-- The empty lazy list. -/
   | nil : LazyList α
   /-- Construct a lazy list from an element and a tail inside a thunk. -/
   | cons (hd : α) (tl : Thunk <| LazyList α) : LazyList α
 
 
+set_option linter.deprecated false
 namespace LazyList