Simplifying a bitvector constant

Stream: lean4

[Juneyoung Lee]

Hi all, what would be a short solution for this problem that involves a big bit-vector constant?

import Std.Data.BitVec.Basic

open Std.BitVec

example: ∃ y', Std.BitVec.toNat (signExtend 64 126#7) = y' <<< 1 := by
  -- The below tactic raises 'maximum recursion depth has been reached'
  -- simp (config := { ground := true})
  sorry

[James Gallicchio]

I think there's a thread somewhere about normalizing bitvectors? let me look

[James Gallicchio]

I do not see it, sorry :frowning:

[Kim Morrison]

We're aware of some problems with config := { ground := true } giving similar errors, and Leo is looking into them in the next few days.

[Kim Morrison]

@Juneyoung Lee, Leo's updates have just landed, and if you change your toolchain to leanprover/lean4:nightly-2024-02-18 this problem has been resolved.

[Kim Morrison]

You can find a version of Std compatible with this toolchain at the tag nightly-testing-2024-02-18. (i.e. you can put that in your lakefile instead of main)