Communicating Lean search paths between processes

structure Lean.LeanPaths : Type

• oleanPath : Lean.SearchPath
• srcPath : Lean.SearchPath
• loadDynlibPaths : Array System.FilePath

instance Lean.instToJsonLeanPaths : Lean.ToJson Lean.LeanPaths

Equations

• Lean.instToJsonLeanPaths = { toJson := Lean.toJsonLeanPaths✝ }

instance Lean.instFromJsonLeanPaths : Lean.FromJson Lean.LeanPaths

Equations

• Lean.instFromJsonLeanPaths = { fromJson? := Lean.fromJsonLeanPaths✝ }

def Lean.initSrcSearchPath (pkgSearchPath : Lean.SearchPath := ∅) : IO Lean.SearchPath

Equations

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