UInt reduceBEq is hidden

Stream: lean4

[Pavel Klimov]

Simproc UInt32.reduceBEq and similar are hidden
https://github.com/leanprover/lean4/blob/8f80d2c2e0441b7ead0fe9dd889375c1180b2c68/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean#L55
It happens because of hygiene mechanism in macros.

So, as far as I understand, there is no way to use it in simp only syntax. Only when you use simp with all simp power you can use it. I know you can disable some transformations, but anyway. Is there any reason behind, why UInt32.reduceBEq and similar are hidden?

Examples.

The following is working:

example (h : (2347861 == 522312) = true) : 1 = 2 := by
  simp only [Nat.reduceBEq, Bool.false_eq_true] at h

while following doesn't:

example (h : ((2347861 : UInt32) == (522312 : UInt32)) = true) : 1 = 2 := by
  simp only [UInt32.reduceBEq, Bool.false_eq_true] at h

[Markus Himmel]

Thank you for the report. Would you mind reporting this as a bug over at https://github.com/leanprover/lean4/issues ?