Documentation

Init.Data.UInt.Log2

@[extern lean_uint8_log2]
Equations
  • a.log2 = { val := a.val.log2 }
Instances For
    @[extern lean_uint16_log2]
    Equations
    • a.log2 = { val := a.val.log2 }
    Instances For
      @[extern lean_uint32_log2]
      Equations
      • a.log2 = { val := a.val.log2 }
      Instances For
        @[extern lean_uint64_log2]
        Equations
        • a.log2 = { val := a.val.log2 }
        Instances For
          @[extern lean_usize_log2]
          Equations
          • a.log2 = { val := a.val.log2 }
          Instances For