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