This module contains the implementation of the pre processing pass for reducing UIntX/IntX to BitVec and thus allow bv_decide to reason about them.

It:

1. runs the int_toBitVec simp set
2. If USize.toBitVec/ISize.toBitVec is used anywhere looks for equations of the form System.Platform.numBits = constant (or flipped) and uses them to convert the system back to fixed width.

def Lean.Meta.Tactic.BVDecide.Normalize.intToBitVecPass : Pass

Equations

• One or more equations did not get rendered due to their size.