fix: disable USize simprocs

leanprover · Feb 24, 2024 · 0e254f1 · 0e254f1
1 parent d179d6c
commit 0e254f1
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/Lean/Meta/Match/Value.lean b/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 :=

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/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
diff --git a/tests/lean/run/no_simproc_usize.lean b/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