structure BitVec.Literal : Type

A bit-vector literal

• n : Nat

  Size.

• value : BitVec self.n

  Actual value.

instance BitVec.instDecidableEqLiteral : DecidableEq BitVec.Literal

Equations

• BitVec.instDecidableEqLiteral = BitVec.decEqLiteral✝

instance BitVec.instReprLiteral : Repr BitVec.Literal

Equations

• BitVec.instReprLiteral = { reprPrec := BitVec.reprLiteral✝ }

def BitVec.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option BitVec.Literal)

Try to convert OfNat.ofNat/BitVec.OfNat application into a bitvector literal.

Equations

• BitVec.fromExpr? e = do let __discr ← liftM (Lean.Meta.getBitVecValue? e) match __discr with | some ⟨n, value⟩ => pure (some { n := n, value := value }) | x => pure none

@[inline]

def BitVec.reduceUnary (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous unary bitvector operators.

Equations

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

@[inline]

def BitVec.reduceBin (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing homogeneous binary bitvector operators.

Equations

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

@[inline]

def BitVec.reduceExtend (declName : Lake.Name) (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Simplification procedure for setWidth, zeroExtend and signExtend on BitVecs.

Equations

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

@[inline]

def BitVec.reduceGetBit (declName : Lake.Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as getLsb and getMsb.

Equations

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

@[inline]

def BitVec.reduceShift (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing bitvector functions such as shiftLeft and rotateRight.

Equations

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

@[inline]

def BitVec.reduceShiftWithBitVecLit (declName : Lake.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Helper function for reducing x <<< i and x >>> i where i is a bitvector literal, into one that is a natural number literal.

Equations

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

@[inline]

def BitVec.reduceBinPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing bitvector predicates.

Equations

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

@[inline]

def BitVec.reduceBoolPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

Equations

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

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.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.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.reduceExtracLsb' : 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.

@[inline]

def BitVec.reduceShiftShift (declName : Lake.Name) (thmName : Lake.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Helper function for reducing (x <<< i) <<< j (and (x >>> i) >>> j) where i and j are natural number literals.

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