lazy sequences

Stream: Is there code for X?

[Sacha Ayoun]

Hello, is there an equivalent of OCaml’s Seq.t?
I could easily just re-implement it but I’m surprised not to find an equivalent, I’m new to Lean, I expect I don’t understand some documentation somewhere
At first I thought lists could be lazy already, a la Haskell, but then I learned that Lean is strict

[Aaron Liu]

Try docs#MLList

[Sacha Ayoun]

That feels somewhat much heavier than what I need, I’d like to see how performant I can get this code (and if I can get it on par with the OCaml impl).
Though I guess some of the variants will just be unused and that’s fine

[Sacha Ayoun]

I’ll try it, thank you @Aaron Liu

[Kim Morrison]

Yes, MLList is not very performant. :-(