@[extern lean_system_platform_windows]

opaque System.Platform.getIsWindows : Unit → Bool

Checks whether the current platform is Windows.

@[extern lean_system_platform_osx]

opaque System.Platform.getIsOSX : Unit → Bool

Checks whether the current platform is macOS.

@[extern lean_system_platform_emscripten]

opaque System.Platform.getIsEmscripten : Unit → Bool

Checks whether the current platform is Emscripten.

def System.Platform.isWindows : Bool

Is the current platform Windows?

Equations

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

def System.Platform.isOSX : Bool

Is the current platform macOS?

Equations

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

def System.Platform.isEmscripten : Bool

Is the current platform Emscripten?

Equations

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

@[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.

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

@[simp]

theorem System.Platform.numBits_pos : 0 < numBits

@[simp]

theorem System.Platform.le_numBits : 32 ≤ numBits

@[simp]

theorem System.Platform.numBits_le : numBits ≤ 64

@[simp]

theorem System.Platform.eight_le_numBits : 8 ≤ numBits

@[simp]

theorem System.Platform.sixteen_le_numBits : 16 ≤ numBits

@[simp]

theorem System.Platform.eight_dvd_numBits : 8 ∣ numBits

@[simp]

theorem System.Platform.System.Platform.sixteen_dvd_numBits : 16 ∣ numBits

@[simp]

theorem System.Platform.System.Platform.dvd_numBits : 32 ∣ numBits

@[simp]

theorem System.Platform.System.Platform.numBits_dvd : numBits ∣ 64

instance System.Platform.instNeZeroNatNumBits : NeZero numBits