Documentation

Mathlib.Data.MLList.IO

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

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

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

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

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

    Instances For
      source
      def MLList.runCmd (cmd : String) (args : Array String) (input : optParam String "") :
      MLList IO String

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

      Instances For
        source
        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 })
        Instances For