Documentation

Lean.Util.Paths

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 := [anonymous] }

instance Lean.instFromJsonLeanPaths:

Lean.FromJson Lean.LeanPaths

Equations

Lean.instFromJsonLeanPaths = { fromJson? := [anonymous] }

def Lean.initSrcSearchPath (leanSysroot : System.FilePath) (sp : optParam Lean.SearchPath ∅) :

IO Lean.SearchPath

Equations

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