@[implicit_reducible]

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

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)

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)

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)

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

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