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 && !String.isEmpty Lean.githash) = true then String.take Lean.githash 7 else "src"

def Lake.versionStringCore : String

Equations

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

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 ")"