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

Equations

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

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

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

instance BitVec.instLawfulOrderLT_1 {n : Nat} : Std.LawfulOrderLT (BitVec n)

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

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

instance BitVec.instLawfulUpwardEnumerableLowerBoundClosed {n : Nat} : Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed (BitVec n)

instance BitVec.instLawfulUpwardEnumerableUpperBoundClosed {n : Nat} : Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed (BitVec n)

instance BitVec.instLawfulUpwardEnumerableLowerBoundOpen {n : Nat} : Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open (BitVec n)

instance BitVec.instLawfulUpwardEnumerableUpperBoundOpen {n : Nat} : Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open (BitVec n)

instance BitVec.instRangeSizeClosed {n : Nat} : Std.PRange.RangeSize Std.PRange.BoundShape.closed (BitVec n)

Equations

• BitVec.instRangeSizeClosed = { size := fun (bound : Std.PRange.Bound Std.PRange.BoundShape.closed (BitVec n)) (a : BitVec n) => BitVec.toNat bound + 1 - a.toNat }

instance BitVec.instRangeSizeOpen {n : Nat} : Std.PRange.RangeSize Std.PRange.BoundShape.open (BitVec n)

Equations

• BitVec.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance BitVec.instLawfulRangeSizeClosed {n : Nat} : Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed (BitVec n)

instance BitVec.instLawfulRangeSizeOpen {n : Nat} : Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open (BitVec n)