def BitVec.reduceNeg : Lean.Meta.Simp.DSimproc

Simplification procedure for negation of BitVecs.

def BitVec.reduceNot : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise not of BitVecs.

def BitVec.reduceAbs : Lean.Meta.Simp.DSimproc

Simplification procedure for absolute value of BitVecs.

def BitVec.reduceAnd : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise and of BitVecs.

def BitVec.reduceOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise or of BitVecs.

def BitVec.reduceXOr : Lean.Meta.Simp.DSimproc

Simplification procedure for bitwise xor of BitVecs.

def BitVec.reduceAdd : Lean.Meta.Simp.DSimproc

Simplification procedure for addition of BitVecs.

def BitVec.reduceMul : Lean.Meta.Simp.DSimproc

Simplification procedure for multiplication of BitVecs.

def BitVec.reduceSub : Lean.Meta.Simp.DSimproc

Simplification procedure for subtraction of BitVecs.

def BitVec.reduceDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs.

def BitVec.reduceMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the modulo operation on BitVecs.

def BitVec.reduceUMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the unsigned modulo operation on BitVecs.

def BitVec.reduceUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned division of BitVecs.

def BitVec.reduceSMTUDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for division of BitVecs using the SMT-LIB conventions.

def BitVec.reduceSMod : Lean.Meta.Simp.DSimproc

Simplification procedure for the signed modulo operation on BitVecs.

def BitVec.reduceSRem : Lean.Meta.Simp.DSimproc

Simplification procedure for signed remainder of BitVecs.

def BitVec.reduceSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed t-division of BitVecs.

def BitVec.reduceSMTSDiv : Lean.Meta.Simp.DSimproc

Simplification procedure for signed division of BitVecs using the SMT-LIB conventions.

def BitVec.reduceGetLsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getLsb (lowest significant bit) on BitVec.

def BitVec.reduceGetMsb : Lean.Meta.Simp.DSimproc

Simplification procedure for getMsb (most significant bit) on BitVec.

def BitVec.reduceClz : Lean.Meta.Simp.DSimproc

Simplification procedure for clz (count leading zeros) on BitVec.

def BitVec.reduceCpop : Lean.Meta.Simp.DSimproc

Simplification procedure for cpop (population count) on BitVec.

def BitVec.reduceGetElem : Lean.Meta.Simp.DSimproc

Simplification procedure for getElem on BitVec.

def BitVec.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def BitVec.reduceUShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned shift right on BitVec.

def BitVec.reduceSShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for signed shift right on BitVec.

def BitVec.reduceHShiftLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for shift left on BitVec.

def BitVec.reduceHShiftLeft' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def BitVec.reduceHShiftRight : Lean.Meta.Simp.DSimproc

Simplification procedure for shift right on BitVec.

def BitVec.reduceHShiftRight' : Lean.Meta.Simp.DSimproc

Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

def BitVec.reduceRotateLeft : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate left on BitVec.

def BitVec.reduceRotateRight : Lean.Meta.Simp.DSimproc

Simplification procedure for rotate right on BitVec.

def BitVec.reduceAppend : Lean.Meta.Simp.DSimproc

Simplification procedure for append on BitVec.

def BitVec.reduceCast : Lean.Meta.Simp.DSimproc

Simplification procedure for casting BitVecs along an equality of the size.

def BitVec.reduceToNat : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toNat.

def BitVec.reduceToInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.toInt.

def BitVec.reduceOfInt : Lean.Meta.Simp.DSimproc

Simplification procedure for BitVec.ofInt.

def BitVec.reduceOfNat : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring BitVec.ofNat literals are normalized.

def BitVec.isValue : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring OfNat.ofNat bitvector literals are normalized. For example, (17 : BitVec 4) is reduced to (1 : BitVec 4) when bitVecOfNat := false, and to 1#4 when bitVecOfNat := true.

def BitVec.reduceEq : Lean.Meta.Simp.Simproc

Simplification procedure for = on BitVecs.

def BitVec.reduceNe : Lean.Meta.Simp.Simproc

Simplification procedure for ≠ on BitVecs.

def BitVec.reduceBEq : Lean.Meta.Simp.DSimproc

Simplification procedure for == on BitVecs.

def BitVec.reduceBNe : Lean.Meta.Simp.DSimproc

Simplification procedure for != on BitVecs.

def BitVec.reduceLT : Lean.Meta.Simp.Simproc

Simplification procedure for < on BitVecs.

def BitVec.reduceLE : Lean.Meta.Simp.Simproc

Simplification procedure for ≤ on BitVecs.

def BitVec.reduceGT : Lean.Meta.Simp.Simproc

Simplification procedure for > on BitVecs.

def BitVec.reduceGE : Lean.Meta.Simp.Simproc

Simplification procedure for ≥ on BitVecs.

def BitVec.reduceULT : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than ult on BitVecs.

def BitVec.reduceULE : Lean.Meta.Simp.DSimproc

Simplification procedure for unsigned less than or equal ule on BitVecs.

def BitVec.reduceSLT : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than slt on BitVecs.

def BitVec.reduceSLE : Lean.Meta.Simp.DSimproc

Simplification procedure for signed less than or equal sle on BitVecs.

def BitVec.reduceSetWidth' : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth' on BitVecs.

def BitVec.reduceShiftLeftZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for shiftLeftZeroExtend on BitVecs.

def BitVec.reduceExtractLsb' : Lean.Meta.Simp.DSimproc

Simplification procedure for extractLsb' on BitVecs.

def BitVec.reduceExtractLsb : Lean.Meta.Simp.DSimproc

Simplification procedure for extractLsb on BitVecs.

def BitVec.reduceReplicate : Lean.Meta.Simp.DSimproc

Simplification procedure for replicate on BitVecs.

def BitVec.reduceSetWidth : Lean.Meta.Simp.DSimproc

Simplification procedure for setWidth on BitVecs.

def BitVec.reduceZeroExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for zeroExtend on BitVecs.

def BitVec.reduceSignExtend : Lean.Meta.Simp.DSimproc

Simplification procedure for signExtend on BitVecs.

def BitVec.reduceAllOnes : Lean.Meta.Simp.DSimproc

Simplification procedure for allOnes

def BitVec.reduceBitVecOfFin : Lean.Meta.Simp.DSimproc

def BitVec.reduceBitVecToFin : Lean.Meta.Simp.DSimproc

def BitVec.reduceShiftLeftShiftLeft : Lean.Meta.Simp.Simproc

def BitVec.reduceShiftRightShiftRight : Lean.Meta.Simp.Simproc