← Copula mathematical handbook

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 toString "src+" ++ toString (Lean.githash.take 7) else "src"

def Lake.versionStringCore : String

Equations

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

def Lake.versionString : String

Equations

• Lake.versionString = if Lake.version.specialDesc ≠ "" then toString Lake.versionStringCore ++ toString "-" ++ toString Lake.version.specialDesc else Lake.versionStringCore

def Lake.uiVersionString : String

Equations

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