Documentation
Lean
.
Util
.
Paths
Search
return to top
source
Imports
Lean.Data.Json
Lean.Util.Path
Imported by
Lean
.
LeanPaths
Lean
.
instToJsonLeanPaths
Lean
.
instFromJsonLeanPaths
Communicating Lean search paths between processes
source
structure
Lean
.
LeanPaths
:
Type
oleanPath :
SearchPath
srcPath :
SearchPath
loadDynlibPaths :
Array
System.FilePath
pluginPaths :
Array
System.FilePath
Instances For
source
instance
Lean
.
instToJsonLeanPaths
:
ToJson
LeanPaths
Equations
source
instance
Lean
.
instFromJsonLeanPaths
:
FromJson
LeanPaths
Equations