search

opencompl / lean-mlir

A minimal development of SSA theory
Other
68 stars 6 forks source link

chore: use w instead of w+1 in HackersDelight #589

Closed tobiasgrosser closed 1 week ago

github-actions[bot] commented 1 week ago

Alive Statistics: 67 / 93 (26 failed)

AtticusKuhn commented 1 week ago

@tobiasgrosser There was a reason that the bit-width was w + 1 instead of w.

See https://grosser.zulipchat.com/#narrow/stream/446584-Project---Lean4---BitVectors/topic/Hacker's.20Delight.20.26.20Other.20Lemmas/near/463417442

tobiasgrosser commented 1 week ago

AFAIU, I set them to w+1 because the automata tactic could not support it. As your PR fixed this, we are able to drop it again, no?