Reading from handles, files, and processes as lazy lists.

Deprecation

This material has been moved out of Mathlib to https://github.com/semorrison/lean-monadic-list.

@[deprecated "See deprecation note in module documentation." (since := "2024-08-22")]

def MLList.linesFromHandle (h : IO.FS.Handle) : MLList IO String

Read lines of text from a handle, as a lazy list in IO.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "See deprecation note in module documentation." (since := "2024-08-22")]

def MLList.lines (f : System.FilePath) : MLList IO String

Read lines of text from a file, as a lazy list in IO.

Equations

• MLList.lines f = MLList.squash fun (x : Unit) => do let __do_lift ← IO.FS.Handle.mk f IO.FS.Mode.read pure (MLList.linesFromHandle __do_lift)

@[deprecated "See deprecation note in module documentation." (since := "2024-08-22")]

def MLList.runCmd (cmd : String) (args : Array String) (input : String := "") : MLList IO String

Run a command with given input on stdio, returning stdout as a lazy list in IO.

Equations

• One or more equations did not get rendered due to their size.

def MLList.runCmd.put (child : IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }) (input : String) : IO (IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped })

Equations

• One or more equations did not get rendered due to their size.