Documentation

Init.System.Platform

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
Instances For
    source
    def System.Platform.isOSX :
    Bool

    Is the current platform macOS?

    Equations
    Instances For
      source
      def System.Platform.isEmscripten :
      Bool

      Is the current platform Emscripten?

      Equations
      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
        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