Read file line by line in Lean?

Stream: general

[Fred May]

I found documentation on file streams in lean, but I can't find the actual method to construct any of these types or create a file stream?

[Henrik Böving]

The methods that create streams are right below. As the doc string says these are currently only used for stdin out and err, files use the other types in that module

[Henrik Böving]

And as your actual question seems to be related to reading line by line: there is a getLine function in there

[Fred May]

<deleted>

[Mac Malone]

In addition to stdout/stderr, there is also docs#IO.FS.Stream.ofHandle to create a stream from a file.