`Many` could be more lazy

Thanks a lot for creating this book! It is a great learning resource.

With Many, as defined in chapter 4.3. (Example: Arithmetic in Monads), examples like

#eval (addsTo 15 (.replicate 1000 1)).take 0

quickly crash Lean (error: deep recursion). This can be remedied by changing the definition of Many.union to the one given for Many.orElse in section 5.4.2. (The Alternative Class).

The current definition of Many.bind is:

def Many.bind : Many α → (α → Many β) → Many β
| .none, _ => .none
| .more x xs, f => union (f x) (bind (xs ()) f)

The xs () in the recursive case defeats laziness. With union = orElse it becomes:

def Many.bind : Many α → (α → Many β) → Many β
| .none, _ => .none
| .more x xs, f => union (f x) (fun () => (bind (xs ()) f))

This popped up in #new members > Stuck on ManyT in "Functional Programming in Lean".

Start with the Many definitions and examples in chapter 4.3, then compare Many.union with Many.orElse in section 5.4.2. Reproduce the reported #eval expression with 1000 elements and verify that the lazy definition avoids the deep-recursion failure while preserving the intended Many behavior.