Documentation
Lake
.
Version
Search
return to top
source
Imports
Init.Data.ToString
Imported by
Lake
.
version
.
major
Lake
.
version
.
minor
Lake
.
version
.
patch
Lake
.
version
.
isRelease
Lake
.
version
.
specialDesc
Lake
.
versionStringCore
Lake
.
versionString
Lake
.
uiVersionString
source
def
Lake
.
version
.
major
:
Nat
Equations
Lake.version.major
=
5
Instances For
source
def
Lake
.
version
.
minor
:
Nat
Equations
Lake.version.minor
=
0
Instances For
source
def
Lake
.
version
.
patch
:
Nat
Equations
Lake.version.patch
=
0
Instances For
source
def
Lake
.
version
.
isRelease
:
Bool
Equations
Lake.version.isRelease
=
Lean.version.isRelease
Instances For
source
def
Lake
.
version
.
specialDesc
:
String
Equations
Lake.version.specialDesc
=
if
(
Lake.version.isRelease
&&
!
Lean.githash
.
isEmpty
)
=
true
then
Lean.githash
.
take
7
else
"src"
Instances For
source
def
Lake
.
versionStringCore
:
String
Equations
Lake.versionStringCore
=
toString
""
++
toString
Lake.version.major
++
toString
"."
++
toString
Lake.version.minor
++
toString
"."
++
toString
Lake.version.patch
++
toString
""
Instances For
source
def
Lake
.
versionString
:
String
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lake
.
uiVersionString
:
String
Equations
Lake.uiVersionString
=
toString
"Lake version "
++
toString
Lake.versionString
++
toString
" (Lean version "
++
toString
Lean.versionString
++
toString
")"
Instances For