source
structure BitVec.Literal :
Type

A bit-vector literal

- n : Nat

  Size.

- value : BitVec self.n

  Actual value.

Instances For

source
instance BitVec.instDecidableEqLiteral :
DecidableEq Literal
Equations

- BitVec.instDecidableEqLiteral = BitVec.instDecidableEqLiteral.decEq

source
def BitVec.instDecidableEqLiteral.decEq (x✝ x✝¹ : Literal) :
Decidable (x✝ = x✝¹)
Equations

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

Instances For

source
instance BitVec.instReprLiteral :
Repr Literal
Equations

- BitVec.instReprLiteral = { reprPrec := BitVec.instReprLiteral.repr }

source
def BitVec.instReprLiteral.repr :
Literal → Nat → Std.Format
Equations

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

Instances For

source
def BitVec.fromExpr? (e : Lean.Expr) :
Lean.Meta.SimpM (Option 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

Instances For

source
def BitVec.toExpr' {n : Nat} (a : BitVec n) :
Lean.Meta.SimpM Lean.Expr
Equations

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

Instances For

source
@[inline]
def BitVec.reduceUnary (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceBin (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceExtend (declName : Lean.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 `BitVec`s.

Equations

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

Instances For

source
@[inline]
def BitVec.reduceGetBit (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceShift (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceShiftWithBitVecLit (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceBinPred (declName : Lean.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.

Instances For

source
@[inline]
def BitVec.reduceBoolPred (declName : Lean.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.

Instances For

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

Simplification procedure for negation of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for bitwise not of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for absolute value of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for bitwise and of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for bitwise or of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for bitwise xor of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for addition of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for multiplication of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for subtraction of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for division of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for the modulo operation on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for the unsigned modulo operation on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for unsigned division of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for division of `BitVec`s using the SMT-LIB conventions.

Equations

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

Instances For

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

Simplification procedure for the signed modulo operation on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for signed remainder of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for signed t-division of `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for signed division of `BitVec`s using the SMT-LIB conventions.

Equations

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

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

Simplification procedure for casting `BitVec`s along an equality of the size.

Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

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

Simplification procedure for `=` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `≠` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `==` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `!=` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `<` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `≤` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `>` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `≥` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for unsigned less than `ult` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for unsigned less than or equal `ule` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for signed less than `slt` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for signed less than or equal `sle` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `setWidth'` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `extractLsb'` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `replicate` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `setWidth` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `zeroExtend` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `signExtend` on `BitVec`s.

Equations

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

Instances For

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

Simplification procedure for `allOnes`

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
@[inline]
def BitVec.reduceShiftShift (declName thmName : Lean.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.

Instances For

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

- BitVec.reduceShiftLeftShiftLeft = BitVec.reduceShiftShift `HShiftLeft.hShiftLeft `BitVec.shiftLeft_add

Instances For

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

- BitVec.reduceShiftRightShiftRight = BitVec.reduceShiftShift `HShiftRight.hShiftRight `BitVec.shiftRight_add

Instances For