source
@[extern lean_system_platform_windows]
opaque System.Platform.getIsWindows :
Unit → Bool

Checks whether the current platform is Windows.

source
@[extern lean_system_platform_osx]
opaque System.Platform.getIsOSX :
Unit → Bool

Checks whether the current platform is macOS.

source
@[extern lean_system_platform_emscripten]
opaque System.Platform.getIsEmscripten :
Unit → Bool

Checks whether the current platform is Emscripten.

source
def System.Platform.isWindows :
Bool

Is the current platform Windows?

Equations

- System.Platform.isWindows = System.Platform.getIsWindows ()

Instances For

source
def System.Platform.isOSX :
Bool

Is the current platform macOS?

Equations

- System.Platform.isOSX = System.Platform.getIsOSX ()

Instances For

source
def System.Platform.isEmscripten :
Bool

Is the current platform Emscripten?

Equations

- System.Platform.isEmscripten = System.Platform.getIsEmscripten ()

Instances For

source
@[extern lean_system_platform_target]
opaque System.Platform.getTarget :
Unit → String

Gets the LLVM target triple of the current platform, or `""` if this was missing when Lean was compiled.

source
def System.Platform.target :
String

The LLVM target triple of the current platform. Empty if missing when Lean was compiled.

Equations

- System.Platform.target = System.Platform.getTarget ()

Instances For

source
@[simp]
theorem System.Platform.numBits_pos :
0 < numBits
source
@[simp]
theorem System.Platform.le_numBits :
32 ≤ numBits
source
@[simp]
theorem System.Platform.numBits_le :
numBits ≤ 64
source
@[simp]
theorem System.Platform.eight_le_numBits :
8 ≤ numBits
source
@[simp]
theorem System.Platform.sixteen_le_numBits :
16 ≤ numBits
source
@[simp]
theorem System.Platform.eight_dvd_numBits :
8 ∣ numBits
source
@[simp]
theorem System.Platform.System.Platform.sixteen_dvd_numBits :
16 ∣ numBits
source
@[simp]
theorem System.Platform.System.Platform.dvd_numBits :
32 ∣ numBits
source
@[simp]
theorem System.Platform.System.Platform.numBits_dvd :
numBits ∣ 64
source
instance System.Platform.instNeZeroNatNumBits :
NeZero numBits