Documentation

Lean.Runtime

source
@[extern lean_closure_max_args]
opaque Lean.closureMaxArgsFn :
Unit → Nat
source
@[extern lean_max_small_nat]
opaque Lean.maxSmallNatFn :
Unit → Nat
source
@[extern lean_get_max_ctor_num_objs]
opaque Lean.getMaxCtorNumObjs :
Unit → Nat
source
def Lean.maxCtorNumObjs :
Nat
Instances For
    source
    @[extern lean_get_max_ctor_scalars_size]
    opaque Lean.getMaxCtorScalarsSize :
    Unit → Nat
    source
    def Lean.maxCtorScalarsSize :
    Nat
    Instances For
      source
      @[extern lean_get_max_ctor_tag]
      opaque Lean.getMaxCtorTag :
      Unit → Nat
      source
      def Lean.maxCtorTag :
      Nat
      Instances For
        source
        @[extern lean_get_usize_size]
        opaque Lean.getUSizeSize :
        Unit → Nat
        source
        def Lean.usizeSize :
        Nat
        Instances For
          source
          @[extern lean_libuv_version]
          opaque Lean.libUVVersionFn :
          Unit → Nat
          source
          @[extern lean_openssl_version]
          opaque Lean.openSSLVersionFn :
          Unit → Nat
          source
          def Lean.closureMaxArgs :
          Nat
          Instances For
            source
            def Lean.maxSmallNat :
            Nat
            Instances For
              source
              def Lean.libUVVersion :
              Nat
              Instances For
                source
                def Lean.openSSLVersion :
                Nat
                Instances For