chore: fix conflicts

Author: hargoniX

src/Init/Data/BitVec/BasicAux.lean

@@ -15,7 +15,7 @@ section Nat
 /-- The `BitVec` with value `i mod 2^n`. -/
 @[match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
+  toFin := Fin.ofNat' (2^n) i
 
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 

src/Init/Data/UInt/Basic.lean

@@ -237,11 +237,6 @@ instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
--- This instance would interfere with the global instance `NeZero (n + 1)`,
--- so we only enable it locally.
-@[local instance]
-private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
-
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_usize_div"]

tests/lean/307.lean.expected.out

@@ -17,6 +17,15 @@ Int.ofNat 2
 1
 1
 1
+1
+1
+1
+1
+1
+1
+1
+1
+1
 2147483648
 0
 0
@@ -26,3 +35,8 @@ Int.ofNat 2
 1
 1
 1
+1
+1
+1
+1
+1