porting lazylist

Stream: mathlib4

[Siddhartha Gadgil]

I have made a PR at https://github.com/leanprover-community/mathlib4/pull/653

In Lean 4 functions like head that fall back to defaults have been renamed head!. For now I have not made the corresponding changes. Should I do so?

[Mario Carneiro]

The ! suffix does not mean that it falls back to a default, but rather that it panics in the undefined case

[Mario Carneiro]

headD is for if you have a provided default, and headI for if you want to return default without a panic

[Siddhartha Gadgil]

Thanks. Does that mean that the function should be headI.

[Siddhartha Gadgil]

I assume the priority is downstream dependencies, so best not to change the name. But I was checking.

[Mario Carneiro]

Names can be changed in downstream dependencies using #align. Don't be afraid to do renames, this is the best opportunity to do so

[Siddhartha Gadgil]

Done. There was in fact a #alignjust there in the synported file which I modified.