instance BitVec.instShiftLeft_sSA {n : Nat} : ShiftLeft (BitVec n)

Equations

• BitVec.instShiftLeft_sSA = { shiftLeft := fun (x y : BitVec n) => x <<< y.toNat }

instance BitVec.instShiftRight_sSA {n : Nat} : ShiftRight (BitVec n)

Equations

• BitVec.instShiftRight_sSA = { shiftRight := fun (x y : BitVec n) => x >>> y.toNat }

inductive BitVec.Refinement {α : Type u} : Option α → Option α → Prop

• bothSome: ∀ {α : Type u} {x y : α}, x = y → some x ⊑ some y
• noneAny: ∀ {α : Type u} {x? : Option α}, none ⊑ x?

@[simp]

theorem BitVec.Refinement.some_some {α : Type u} {x : α} {y : α} : some x ⊑ some y ↔ x = y

@[simp]

theorem BitVec.Refinement.none_left : ∀ {α : Type u_1} {x? : Option α}, none ⊑ x?

theorem BitVec.Refinement.none_right {α : Type u_1} {x? : Option α} : x? ⊑ none ↔ x? = none

theorem BitVec.Refinement.some_left {α : Type u_1} {x : α} {y? : Option α} : some x ⊑ y? ↔ y? = some x

@[simp]

theorem BitVec.Refinement.refl {α : Type u} (x : Option α) : x ⊑ x

theorem BitVec.Refinement.trans {α : Type u} (x : Option α) (y : Option α) (z : Option α) : x ⊑ y → y ⊑ z → x ⊑ z

instance BitVec.Refinement.instDecidableRelOptionOfDecidableEq {α : Type u} [DEQ : DecidableEq α] : DecidableRel BitVec.Refinement

Equations

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

instance BitVec.instCoeBoolOfNatNat_sSA : Coe Bool (BitVec 1)

Equations

• BitVec.instCoeBoolOfNatNat_sSA = { coe := BitVec.ofBool }

def BitVec.coeWidth {m : Nat} {n : Nat} : BitVec m → BitVec n

Equations

• x.coeWidth = BitVec.ofNat n x.toNat

instance BitVec.decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1)

Equations

• BitVec.decPropToBitvec1 p = { coe := BitVec.ofBool (decide p) }

theorem BitVec.Int.natCast_pred_of_pos (x : Nat) (h : 0 < x) : ↑x - 1 = ↑(x - 1)