.

src/Init/Data/SInt/Basic.lean

@@ -239,6 +239,17 @@ Examples:
 @[extern "lean_int8_div"]
 protected def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
+The power operation, raising an 8-bit signed integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def Int8.pow (x : Int8) (n : Nat) : Int8 :=
+  match n with
+  | 0 => 1
+  | n + 1 => Int8.mul (Int8.pow x n) x
+/--
 The modulo operator for 8-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int8.div`. Usually accessed via the `%`
 operator.
@@ -366,6 +377,7 @@ instance : Inhabited Int8 where
 instance : Add Int8         := ⟨Int8.add⟩
 instance : Sub Int8         := ⟨Int8.sub⟩
 instance : Mul Int8         := ⟨Int8.mul⟩
+instance : Pow Int8 Nat     := ⟨Int8.pow⟩
 instance : Mod Int8         := ⟨Int8.mod⟩
 instance : Div Int8         := ⟨Int8.div⟩
 instance : LT Int8          := ⟨Int8.lt⟩
@@ -598,6 +610,17 @@ Examples:
 @[extern "lean_int16_div"]
 protected def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
+The power operation, raising a 16-bit signed integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def Int16.pow (x : Int16) (n : Nat) : Int16 :=
+  match n with
+  | 0 => 1
+  | n + 1 => Int16.mul (Int16.pow x n) x
+/--
 The modulo operator for 16-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int16.div`. Usually accessed via the `%`
 operator.
@@ -725,6 +748,7 @@ instance : Inhabited Int16 where
 instance : Add Int16         := ⟨Int16.add⟩
 instance : Sub Int16         := ⟨Int16.sub⟩
 instance : Mul Int16         := ⟨Int16.mul⟩
+instance : Pow Int16 Nat     := ⟨Int16.pow⟩
 instance : Mod Int16         := ⟨Int16.mod⟩
 instance : Div Int16         := ⟨Int16.div⟩
 instance : LT Int16          := ⟨Int16.lt⟩
@@ -973,6 +997,17 @@ Examples:
 @[extern "lean_int32_div"]
 protected def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
+The power operation, raising a 32-bit signed integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def Int32.pow (x : Int32) (n : Nat) : Int32 :=
+  match n with
+  | 0 => 1
+  | n + 1 => Int32.mul (Int32.pow x n) x
+/--
 The modulo operator for 32-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int32.div`. Usually accessed via the `%`
 operator.
@@ -1100,6 +1135,7 @@ instance : Inhabited Int32 where
 instance : Add Int32         := ⟨Int32.add⟩
 instance : Sub Int32         := ⟨Int32.sub⟩
 instance : Mul Int32         := ⟨Int32.mul⟩
+instance : Pow Int32 Nat     := ⟨Int32.pow⟩
 instance : Mod Int32         := ⟨Int32.mod⟩
 instance : Div Int32         := ⟨Int32.div⟩
 instance : LT Int32          := ⟨Int32.lt⟩
@@ -1368,6 +1404,17 @@ Examples:
 @[extern "lean_int64_div"]
 protected def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
+The power operation, raising a 64-bit signed integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def Int64.pow (x : Int64) (n : Nat) : Int64 :=
+  match n with
+  | 0 => 1
+  | n + 1 => Int64.mul (Int64.pow x n) x
+/--
 The modulo operator for 64-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int64.div`. Usually accessed via the `%`
 operator.
@@ -1495,6 +1542,7 @@ instance : Inhabited Int64 where
 instance : Add Int64         := ⟨Int64.add⟩
 instance : Sub Int64         := ⟨Int64.sub⟩
 instance : Mul Int64         := ⟨Int64.mul⟩
+instance : Pow Int64 Nat     := ⟨Int64.pow⟩
 instance : Mod Int64         := ⟨Int64.mod⟩
 instance : Div Int64         := ⟨Int64.div⟩
 instance : LT Int64          := ⟨Int64.lt⟩
@@ -1746,6 +1794,17 @@ Examples:
 @[extern "lean_isize_div"]
 protected def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
+The power operation, raising a word-sized signed integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def ISize.pow (x : ISize) (n : Nat) : ISize :=
+  match n with
+  | 0 => 1
+  | n + 1 => ISize.mul (ISize.pow x n) x
+/--
 The modulo operator for word-sized signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `ISize.div`. Usually accessed via the `%`
 operator.
@@ -1875,6 +1934,7 @@ instance : Inhabited ISize where
 instance : Add ISize         := ⟨ISize.add⟩
 instance : Sub ISize         := ⟨ISize.sub⟩
 instance : Mul ISize         := ⟨ISize.mul⟩
+instance : Pow ISize Nat     := ⟨ISize.pow⟩
 instance : Mod ISize         := ⟨ISize.mod⟩
 instance : Div ISize         := ⟨ISize.div⟩
 instance : LT ISize          := ⟨ISize.lt⟩

src/Init/Data/SInt/Lemmas.lean

@@ -2625,6 +2625,17 @@ instance : Std.LawfulCommIdentity (α := ISize) (· * ·) 1 where
 @[simp] theorem Int64.zero_mul {a : Int64} : 0 * a = 0 := Int64.toBitVec_inj.1 BitVec.zero_mul
 @[simp] theorem ISize.zero_mul {a : ISize} : 0 * a = 0 := ISize.toBitVec_inj.1 BitVec.zero_mul
 
+@[simp] protected theorem Int8.pow_zero (x : Int8) : x ^ 0 = 1 := rfl
+protected theorem Int8.pow_succ (x : Int8) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem Int16.pow_zero (x : Int16) : x ^ 0 = 1 := rfl
+protected theorem Int16.pow_succ (x : Int16) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem Int32.pow_zero (x : Int32) : x ^ 0 = 1 := rfl
+protected theorem Int32.pow_succ (x : Int32) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem Int64.pow_zero (x : Int64) : x ^ 0 = 1 := rfl
+protected theorem Int64.pow_succ (x : Int64) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem ISize.pow_zero (x : ISize) : x ^ 0 = 1 := rfl
+protected theorem ISize.pow_succ (x : ISize) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+
 protected theorem Int8.mul_add {a b c : Int8} : a * (b + c) = a * b + a * c :=
     Int8.toBitVec_inj.1 BitVec.mul_add
 protected theorem Int16.mul_add {a b c : Int16} : a * (b + c) = a * b + a * c :=

src/Init/Data/UInt/Basic.lean

@@ -55,6 +55,17 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint8_div"]
 protected def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
+The power operation, raising an 8-bit unsigned integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def UInt8.pow (x : UInt8) (n : Nat) : UInt8 :=
+  match n with
+  | 0 => 1
+  | n + 1 => UInt8.mul (UInt8.pow x n) x
+/--
 The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -129,6 +140,7 @@ protected def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
+instance : Pow UInt8 Nat   := ⟨UInt8.pow⟩
 instance : Mod UInt8       := ⟨UInt8.mod⟩
 
 set_option linter.deprecated false in
@@ -252,6 +264,17 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint16_div"]
 protected def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
+The power operation, raising a 16-bit unsigned integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def UInt16.pow (x : UInt16) (n : Nat) : UInt16 :=
+  match n with
+  | 0 => 1
+  | n + 1 => UInt16.mul (UInt16.pow x n) x
+/--
 The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -289,7 +312,7 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint16_lor"]
 protected def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
 /--
-Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
+Bitwise exclusive or for 16-bit unsigned integers. Usually accessed via the `^^^` operator.
 
 Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
 integers are set.
@@ -326,6 +349,7 @@ protected def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
+instance : Pow UInt16 Nat   := ⟨UInt16.pow⟩
 instance : Mod UInt16       := ⟨UInt16.mod⟩
 
 set_option linter.deprecated false in
@@ -451,6 +475,17 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint32_div"]
 protected def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
+The power operation, raising a 32-bit unsigned integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def UInt32.pow (x : UInt32) (n : Nat) : UInt32 :=
+  match n with
+  | 0 => 1
+  | n + 1 => UInt32.mul (UInt32.pow x n) x
+/--
 The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -525,6 +560,7 @@ protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
+instance : Pow UInt32 Nat   := ⟨UInt32.pow⟩
 instance : Mod UInt32       := ⟨UInt32.mod⟩
 
 set_option linter.deprecated false in
@@ -612,6 +648,17 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint64_div"]
 protected def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
+The power operation, raising a 64-bit unsigned integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def UInt64.pow (x : UInt64) (n : Nat) : UInt64 :=
+  match n with
+  | 0 => 1
+  | n + 1 => UInt64.mul (UInt64.pow x n) x
+/--
 The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -686,6 +733,7 @@ protected def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
+instance : Pow UInt64 Nat   := ⟨UInt64.pow⟩
 instance : Mod UInt64       := ⟨UInt64.mod⟩
 
 set_option linter.deprecated false in
@@ -706,7 +754,7 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint64_complement"]
 protected def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
 /--
-Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
+Negation of 64-bit unsigned integers, computed modulo `UInt64.size`.
 
 `UInt64.neg a` is equivalent to `18_446_744_073_709_551_615 - a + 1`.
 
@@ -804,6 +852,17 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_usize_div"]
 protected def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 /--
+The power operation, raising a word-sized unsigned integer to a natural number power,
+wrapping around on overflow. Usually accessed via the `^` operator.
+
+This function is currently *not* overridden at runtime with an efficient implementation,
+and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def USize.pow (x : USize) (n : Nat) : USize :=
+  match n with
+  | 0 => 1
+  | n + 1 => USize.mul (USize.pow x n) x
+/--
 The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -937,6 +996,7 @@ def USize.toUInt64 (a : USize) : UInt64 :=
   UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)
 
 instance : Mul USize       := ⟨USize.mul⟩
+instance : Pow USize Nat   := ⟨USize.pow⟩
 instance : Mod USize       := ⟨USize.mod⟩
 
 set_option linter.deprecated false in

src/Init/Data/UInt/Lemmas.lean

@@ -2614,6 +2614,17 @@ instance : Std.LawfulCommIdentity (α := USize) (· * ·) 1 where
 @[simp] theorem UInt64.zero_mul {a : UInt64} : 0 * a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_mul
 @[simp] theorem USize.zero_mul {a : USize} : 0 * a = 0 := USize.toBitVec_inj.1 BitVec.zero_mul
 
+@[simp] protected theorem UInt8.pow_zero (x : UInt8) : x ^ 0 = 1 := rfl
+protected theorem UInt8.pow_succ (x : UInt8) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem UInt16.pow_zero (x : UInt16) : x ^ 0 = 1 := rfl
+protected theorem UInt16.pow_succ (x : UInt16) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem UInt32.pow_zero (x : UInt32) : x ^ 0 = 1 := rfl
+protected theorem UInt32.pow_succ (x : UInt32) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem UInt64.pow_zero (x : UInt64) : x ^ 0 = 1 := rfl
+protected theorem UInt64.pow_succ (x : UInt64) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+@[simp] protected theorem USize.pow_zero (x : USize) : x ^ 0 = 1 := rfl
+protected theorem USize.pow_succ (x : USize) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
+
 protected theorem UInt8.mul_add {a b c : UInt8} : a * (b + c) = a * b + a * c :=
     UInt8.toBitVec_inj.1 BitVec.mul_add
 protected theorem UInt16.mul_add {a b c : UInt16} : a * (b + c) = a * b + a * c :=