def Lake.version.major : Nat

Equations

• Lake.version.major = 5

def Lake.version.minor : Nat

Equations

• Lake.version.minor = 0

def Lake.version.patch : Nat

Equations

• Lake.version.patch = 0

def Lake.version.isRelease : Bool

Equations

• Lake.version.isRelease = Lean.version.isRelease

def Lake.version.specialDesc : String

Equations

• Lake.version.specialDesc = if (Lake.version.isRelease && !Lean.githash.isEmpty) = true then Lean.githash.take 7 else "src"

def Lake.versionStringCore : String

Equations

• Lake.versionStringCore = toString "" ++ toString Lake.version.major ++ toString "." ++ toString Lake.version.minor ++ toString "." ++ toString Lake.version.patch ++ toString ""

def Lake.versionString : String

Equations

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

def Lake.uiVersionString : String

Equations

• Lake.uiVersionString = toString "Lake version " ++ toString Lake.versionString ++ toString " (Lean version " ++ toString Lean.versionString ++ toString ")"