@[implicit_reducible]

instance BitVec.instUpwardEnumerable {n : Nat} : Std.PRange.UpwardEnumerable (BitVec n)

Equations

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

theorem BitVec.succ?_eq_none {n : Nat} {x : BitVec n} : Std.PRange.succ? x = none ↔ x.toNat = 2 ^ n - 1

theorem BitVec.succ?_eq_some {n : Nat} {x y : BitVec n} : Std.PRange.succ? x = some y ↔ x.toNat < 2 ^ n - 1 ∧ y.toNat = x.toNat + 1

instance BitVec.instLawfulUpwardEnumerable {n : Nat} : Std.PRange.LawfulUpwardEnumerable (BitVec n)

instance BitVec.instLawfulUpwardEnumerableLE {n : Nat} : Std.PRange.LawfulUpwardEnumerableLE (BitVec n)

instance BitVec.instLawfulUpwardEnumerableLT {n : Nat} : Std.PRange.LawfulUpwardEnumerableLT (BitVec n)

@[implicit_reducible]

instance BitVec.instRxcHasSize {n : Nat} : Std.Rxc.HasSize (BitVec n)

Equations

• BitVec.instRxcHasSize = { size := fun (lo hi : BitVec n) => hi.toNat + 1 - lo.toNat }

instance BitVec.instRxcLawfulHasSize {n : Nat} : Std.Rxc.LawfulHasSize (BitVec n)

instance BitVec.instRxcIsAlwaysFinite {n : Nat} : Std.Rxc.IsAlwaysFinite (BitVec n)

@[implicit_reducible]

instance BitVec.instRxoHasSize {n : Nat} : Std.Rxo.HasSize (BitVec n)

Equations

• BitVec.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance BitVec.instRxoLawfulHasSize {n : Nat} : Std.Rxo.LawfulHasSize (BitVec n)

instance BitVec.instRxoIsAlwaysFinite {n : Nat} : Std.Rxo.IsAlwaysFinite (BitVec n)

@[implicit_reducible]

instance BitVec.instRxiHasSize {n : Nat} : Std.Rxi.HasSize (BitVec n)

Equations

• BitVec.instRxiHasSize = { size := fun (lo : BitVec n) => 2 ^ n - lo.toNat }

instance BitVec.instRxiLawfulHasSize {n : Nat} : Std.Rxi.LawfulHasSize (BitVec n)

instance BitVec.instRxiIsAlwaysFinite {n : Nat} : Std.Rxi.IsAlwaysFinite (BitVec n)