fix: disable USize simprocs

src/Lean/Meta/Match/Value.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Expr
 
 namespace Lean.Meta
+-- TODO: produce error for `USize` because `USize.decEq` depends on an opaque value: `System.Platform.numBits`.
 
 -- TODO: move?
 private def UIntTypeNames : Array Name :=

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -97,4 +97,8 @@ declare_uint_simprocs UInt8
 declare_uint_simprocs UInt16
 declare_uint_simprocs UInt32
 declare_uint_simprocs UInt64
-declare_uint_simprocs USize
+/-
+We disabled the simprocs for USize since the result of most operations depend on an opaque value: `System.Platform.numBits`.
+We could reduce some cases using the fact that this opaque value is `32` or `64`, but it is unclear whether it would be useful in practice.
+-/
+-- declare_uint_simprocs USize

tests/lean/run/no_simproc_usize.lean

@@ -0,0 +1,3 @@
+example : (10 : USize) + 2 = 12 := by
+  fail_if_success simp -- We don't have USize simprocs since operations depend on `System.Platform.numBits`
+  sorry