Documentation

Lean.Util.FileSetupInfo

source
structure Lean.FileSetupInfo :
Type

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

Instances For
    source
    instance Lean.instFromJsonFileSetupInfo :
    Lean.FromJson Lean.FileSetupInfo
    source
    instance Lean.instToJsonFileSetupInfo :
    Lean.ToJson Lean.FileSetupInfo