structure Lean.FileSetupInfo : Type

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

• paths : Lean.LeanPaths
• setupOptions : Lean.LeanOptions

instance Lean.instFromJsonFileSetupInfo : Lean.FromJson Lean.FileSetupInfo

Equations

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

instance Lean.instToJsonFileSetupInfo : Lean.ToJson Lean.FileSetupInfo

Equations

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