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

Simplification procedure for negation of BitVecs.

Equations

• BitVec.reduceNeg = BitVec.reduceUnary✝ `Neg.neg 3 fun {n : Nat} (x : BitVec n) => -x

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

Simplification procedure for bitwise not of BitVecs.

Equations

• BitVec.reduceNot = BitVec.reduceUnary✝ `Complement.complement 3 fun {n : Nat} (x : BitVec n) => ~~~x

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

Simplification procedure for absolute value of BitVecs.

Equations

• BitVec.reduceAbs = BitVec.reduceUnary✝ `BitVec.abs 2 fun {n : Nat} => BitVec.abs

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

Simplification procedure for bitwise and of BitVecs.

Equations

• BitVec.reduceAnd = BitVec.reduceBin✝ `HAnd.hAnd 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 &&& x2

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

Simplification procedure for bitwise or of BitVecs.

Equations

• BitVec.reduceOr = BitVec.reduceBin✝ `HOr.hOr 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 ||| x2

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

Simplification procedure for bitwise xor of BitVecs.

Equations

• BitVec.reduceXOr = BitVec.reduceBin✝ `HXor.hXor 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 ^^^ x2

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

Simplification procedure for addition of BitVecs.

Equations

• BitVec.reduceAdd = BitVec.reduceBin✝ `HAdd.hAdd 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 + x2

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

Simplification procedure for multiplication of BitVecs.

Equations

• BitVec.reduceMul = BitVec.reduceBin✝ `HMul.hMul 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 * x2

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

Simplification procedure for subtraction of BitVecs.

Equations

• BitVec.reduceSub = BitVec.reduceBin✝ `HSub.hSub 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 - x2

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

Simplification procedure for division of BitVecs.

Equations

• BitVec.reduceDiv = BitVec.reduceBin✝ `HDiv.hDiv 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 / x2

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

Simplification procedure for the modulo operation on BitVecs.

Equations

• BitVec.reduceMod = BitVec.reduceBin✝ `HMod.hMod 6 fun {n : Nat} (x1 x2 : BitVec n) => x1 % x2

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

Simplification procedure for the unsigned modulo operation on BitVecs.

Equations

• BitVec.reduceUMod = BitVec.reduceBin✝ `BitVec.umod 3 fun {n : Nat} => BitVec.umod

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

Simplification procedure for unsigned division of BitVecs.

Equations

• BitVec.reduceUDiv = BitVec.reduceBin✝ `BitVec.udiv 3 fun {n : Nat} => BitVec.udiv

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

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

Equations

• BitVec.reduceSMTUDiv = BitVec.reduceBin✝ `BitVec.smtUDiv 3 fun {n : Nat} => BitVec.smtUDiv

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

Simplification procedure for the signed modulo operation on BitVecs.

Equations

• BitVec.reduceSMod = BitVec.reduceBin✝ `BitVec.smod 3 fun {n : Nat} => BitVec.smod

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

Simplification procedure for signed remainder of BitVecs.

Equations

• BitVec.reduceSRem = BitVec.reduceBin✝ `BitVec.srem 3 fun {n : Nat} => BitVec.srem

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

Simplification procedure for signed t-division of BitVecs.

Equations

• BitVec.reduceSDiv = BitVec.reduceBin✝ `BitVec.sdiv 3 fun {n : Nat} => BitVec.sdiv

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

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

Equations

• BitVec.reduceSMTSDiv = BitVec.reduceBin✝ `BitVec.smtSDiv 3 fun {n : Nat} => BitVec.smtSDiv

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

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

Equations

• BitVec.reduceGetLsb = BitVec.reduceGetBit✝ `BitVec.getLsbD fun {n : Nat} => BitVec.getLsbD

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

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

Equations

• BitVec.reduceGetMsb = BitVec.reduceGetBit✝ `BitVec.getMsbD fun {n : Nat} => BitVec.getMsbD

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

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

Equations

• BitVec.reduceClz = BitVec.reduceUnary✝ `BitVec.clz 2 fun {n : Nat} => BitVec.clz

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

Simplification procedure for cpop (population count) on BitVec.

Equations

• BitVec.reduceCpop = BitVec.reduceUnary✝ `BitVec.cpop 2 fun {n : Nat} => BitVec.cpop

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

Simplification procedure for getElem on BitVec.

Equations

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

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

Simplification procedure for shift left on BitVec.

Equations

• BitVec.reduceShiftLeft = BitVec.reduceShift✝ `BitVec.shiftLeft 3 fun {n : Nat} => BitVec.shiftLeft

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

Simplification procedure for unsigned shift right on BitVec.

Equations

• BitVec.reduceUShiftRight = BitVec.reduceShift✝ `BitVec.ushiftRight 3 fun {n : Nat} => BitVec.ushiftRight

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

Simplification procedure for signed shift right on BitVec.

Equations

• BitVec.reduceSShiftRight = BitVec.reduceShift✝ `BitVec.sshiftRight 3 fun {n : Nat} => BitVec.sshiftRight

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

Simplification procedure for shift left on BitVec.

Equations

• BitVec.reduceHShiftLeft = BitVec.reduceShift✝ `HShiftLeft.hShiftLeft 6 fun {n : Nat} (x1 : BitVec n) (x2 : Nat) => x1 <<< x2

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

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

Equations

• BitVec.reduceHShiftLeft' = BitVec.reduceShiftWithBitVecLit✝ `HShiftLeft.hShiftLeft

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

Simplification procedure for shift right on BitVec.

Equations

• BitVec.reduceHShiftRight = BitVec.reduceShift✝ `HShiftRight.hShiftRight 6 fun {n : Nat} (x1 : BitVec n) (x2 : Nat) => x1 >>> x2

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

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

Equations

• BitVec.reduceHShiftRight' = BitVec.reduceShiftWithBitVecLit✝ `HShiftRight.hShiftRight

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

Simplification procedure for rotate left on BitVec.

Equations

• BitVec.reduceRotateLeft = BitVec.reduceShift✝ `BitVec.rotateLeft 3 fun {n : Nat} => BitVec.rotateLeft

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

Simplification procedure for rotate right on BitVec.

Equations

• BitVec.reduceRotateRight = BitVec.reduceShift✝ `BitVec.rotateRight 3 fun {n : Nat} => BitVec.rotateRight

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

Simplification procedure for append on BitVec.

Equations

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

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

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

Equations

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

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

Simplification procedure for BitVec.toNat.

Equations

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

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

Simplification procedure for BitVec.toInt.

Equations

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

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

Simplification procedure for BitVec.ofInt.

Equations

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

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

Simplification procedure for ensuring BitVec.ofNat literals are normalized.

Equations

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

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.

Equations

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

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

Simplification procedure for = on BitVecs.

Equations

• BitVec.reduceEq = BitVec.reduceBinPred✝ `Eq 3 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 = x2)

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

Simplification procedure for ≠ on BitVecs.

Equations

• BitVec.reduceNe = BitVec.reduceBinPred✝ `Ne 3 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 ≠ x2)

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

Simplification procedure for == on BitVecs.

Equations

• BitVec.reduceBEq = BitVec.reduceBoolPred✝ `BEq.beq 4 fun {n : Nat} (x1 x2 : BitVec n) => x1 == x2

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

Simplification procedure for != on BitVecs.

Equations

• BitVec.reduceBNe = BitVec.reduceBoolPred✝ `bne 4 fun {n : Nat} (x1 x2 : BitVec n) => x1 != x2

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

Simplification procedure for < on BitVecs.

Equations

• BitVec.reduceLT = BitVec.reduceBinPred✝ `LT.lt 4 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 < x2)

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

Simplification procedure for ≤ on BitVecs.

Equations

• BitVec.reduceLE = BitVec.reduceBinPred✝ `LE.le 4 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 ≤ x2)

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

Simplification procedure for > on BitVecs.

Equations

• BitVec.reduceGT = BitVec.reduceBinPred✝ `GT.gt 4 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 > x2)

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

Simplification procedure for ≥ on BitVecs.

Equations

• BitVec.reduceGE = BitVec.reduceBinPred✝ `GE.ge 4 fun {n : Nat} (x1 x2 : BitVec n) => decide (x1 ≥ x2)

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

Simplification procedure for unsigned less than ult on BitVecs.

Equations

• BitVec.reduceULT = BitVec.reduceBoolPred✝ `BitVec.ult 3 fun {n : Nat} => BitVec.ult

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

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

Equations

• BitVec.reduceULE = BitVec.reduceBoolPred✝ `BitVec.ule 3 fun {n : Nat} => BitVec.ule

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

Simplification procedure for signed less than slt on BitVecs.

Equations

• BitVec.reduceSLT = BitVec.reduceBoolPred✝ `BitVec.slt 3 fun {n : Nat} => BitVec.slt

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

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

Equations

• BitVec.reduceSLE = BitVec.reduceBoolPred✝ `BitVec.sle 3 fun {n : Nat} => BitVec.sle

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

Simplification procedure for setWidth' on BitVecs.

Equations

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

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

Simplification procedure for shiftLeftZeroExtend on BitVecs.

Equations

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

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

Simplification procedure for extractLsb' on BitVecs.

Equations

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

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

Simplification procedure for extractLsb on BitVecs.

Equations

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

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

Simplification procedure for replicate on BitVecs.

Equations

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

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

Simplification procedure for setWidth on BitVecs.

Equations

• BitVec.reduceSetWidth = BitVec.reduceExtend✝ `BitVec.setWidth fun {n : Nat} => BitVec.setWidth

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

Simplification procedure for zeroExtend on BitVecs.

Equations

• BitVec.reduceZeroExtend = BitVec.reduceExtend✝ `BitVec.zeroExtend fun {n : Nat} => BitVec.zeroExtend

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

Simplification procedure for signExtend on BitVecs.

Equations

• BitVec.reduceSignExtend = BitVec.reduceExtend✝ `BitVec.signExtend fun {n : Nat} => BitVec.signExtend

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

Simplification procedure for allOnes

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• BitVec.reduceShiftLeftShiftLeft = BitVec.reduceShiftShift✝ `HShiftLeft.hShiftLeft `BitVec.shiftLeft_add

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

Equations

• BitVec.reduceShiftRightShiftRight = BitVec.reduceShiftShift✝ `HShiftRight.hShiftRight `BitVec.shiftRight_add