Communicating Lean search paths between processes

structure Lean.LeanPaths : Type

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

Instances For

• Lean.instFromJsonLeanPaths
• Lean.instToJsonLeanPaths

instance Lean.instToJsonLeanPaths : ToJson LeanPaths

Equations

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

instance Lean.instFromJsonLeanPaths : FromJson LeanPaths

Equations

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