search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

b >>> a.toNat <<< a.toNat = b &&& BitVec.allOnes w <<< a.toNat #604

Closed tobiasgrosser closed 1 month ago

tobiasgrosser commented 1 month ago

This will proof bitvec_InstCombineShift__279 in AliveStatements.