structure Lean.FileSetupInfo : Type

Information shared between Lake and Lean when calling lake setup-file.

• paths : LeanPaths
• setupOptions : LeanOptions

instance Lean.instFromJsonFileSetupInfo : FromJson FileSetupInfo

Equations

• Lean.instFromJsonFileSetupInfo = { fromJson? := Lean.fromJsonFileSetupInfo✝ }

instance Lean.instToJsonFileSetupInfo : ToJson FileSetupInfo

Equations

• Lean.instToJsonFileSetupInfo = { toJson := Lean.toJsonFileSetupInfo✝ }