Documentation

Init.Data.UInt.Log2

@[extern lean_uint8_log2]

Base-two logarithm of 8-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

Equations
    Instances For
      @[extern lean_uint16_log2]

      Base-two logarithm of 16-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

      This function is overridden at runtime with an efficient implementation. This definition is the logical model.

      Examples:

      Equations
        Instances For
          @[extern lean_uint32_log2]

          Base-two logarithm of 32-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

          This function is overridden at runtime with an efficient implementation. This definition is the logical model.

          Examples:

          Equations
            Instances For
              @[extern lean_uint64_log2]

              Base-two logarithm of 64-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

              This function is overridden at runtime with an efficient implementation. This definition is the logical model.

              Examples:

              Equations
                Instances For
                  @[extern lean_usize_log2]

                  Base-two logarithm of word-sized unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

                  This function is overridden at runtime with an efficient implementation. This definition is the logical model.

                  Examples:

                  Equations
                    Instances For