Documentation

Lean.Server.FileWorker

Equations
partial def Lean.Server.FileWorker.lakeSetupSearchPath.processStderr (lakePath : System.FilePath) (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) (args : Array String) (lakeProc : IO.Process.Child { toStdioConfig := { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }, cmd := lakePath.toString, args := args, cwd := none, env := #[] }.toStdioConfig) (acc : String) :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.Server.FileWorker.parseParams (paramType : Type) [inst : Lean.FromJson paramType] (params : Lean.Json) :
Equations
Equations
Equations
Equations
Equations