Documentation

Lean.Meta.Tactic.BVDecide.Normalize.IntToBitVec

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.
source
def Lean.Meta.Tactic.BVDecide.Normalize.addIntToBitVecLemmas (goal : MVarId) (methods : Sym.Simp.Methods) :
PreProcessM Sym.Simp.Methods
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Tactic.BVDecide.Normalize.intToBitVecPass :
    Pass
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For