Documentation

Init.Data.Range.Polymorphic.UInt

instance UInt8.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt8

Equations

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

theorem UInt8.succ?_ofBitVec {x : BitVec 8} :

Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt8.succMany?_ofBitVec {k : Nat} {x : BitVec 8} :

Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt8.upwardEnumerableLE_ofBitVec {x y : BitVec 8} :

Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt8.upwardEnumerableLT_ofBitVec {x y : BitVec 8} :

Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt8.instLawfulUpwardEnumerable :

Std.PRange.LawfulUpwardEnumerable UInt8

instance UInt8.instLawfulUpwardEnumerableLE :

Std.PRange.LawfulUpwardEnumerableLE UInt8

instance UInt8.instLawfulOrderLT_1 :

Std.LawfulOrderLT UInt8

instance UInt8.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt8

instance UInt8.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt8

instance UInt8.instLawfulUpwardEnumerableLowerBoundClosed :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed UInt8

instance UInt8.instLawfulUpwardEnumerableUpperBoundClosed :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed UInt8

instance UInt8.instLawfulUpwardEnumerableLowerBoundOpen :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open UInt8

instance UInt8.instLawfulUpwardEnumerableUpperBoundOpen :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open UInt8

instance UInt8.instRangeSizeClosed :

Std.PRange.RangeSize Std.PRange.BoundShape.closed UInt8

Equations

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

theorem UInt8.rangeSizeSize_eq_toBitVec {bound : Std.PRange.Bound Std.PRange.BoundShape.closed UInt8} {x : BitVec 8} :

Std.PRange.RangeSize.size bound { toBitVec := x } = Std.PRange.RangeSize.size bound.toBitVec x

instance UInt8.instLawfulRangeSizeClosed :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed UInt8

instance UInt8.instRangeSizeOpen :

Std.PRange.RangeSize Std.PRange.BoundShape.open UInt8

Equations

UInt8.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance UInt8.instLawfulRangeSizeOpen :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open UInt8

instance UInt16.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt16

Equations

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

theorem UInt16.succ?_ofBitVec {x : BitVec 16} :

Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt16.succMany?_ofBitVec {k : Nat} {x : BitVec 16} :

Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt16.upwardEnumerableLE_ofBitVec {x y : BitVec 16} :

Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt16.upwardEnumerableLT_ofBitVec {x y : BitVec 16} :

Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt16.instLawfulUpwardEnumerable :

Std.PRange.LawfulUpwardEnumerable UInt16

instance UInt16.instLawfulUpwardEnumerableLE :

Std.PRange.LawfulUpwardEnumerableLE UInt16

instance UInt16.instLawfulOrderLT_1 :

Std.LawfulOrderLT UInt16

instance UInt16.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt16

instance UInt16.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt16

instance UInt16.instLawfulUpwardEnumerableLowerBoundClosed :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed UInt16

instance UInt16.instLawfulUpwardEnumerableUpperBoundClosed :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed UInt16

instance UInt16.instLawfulUpwardEnumerableLowerBoundOpen :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open UInt16

instance UInt16.instLawfulUpwardEnumerableUpperBoundOpen :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open UInt16

instance UInt16.instRangeSizeClosed :

Std.PRange.RangeSize Std.PRange.BoundShape.closed UInt16

Equations

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

theorem UInt16.rangeSizeSize_eq_toBitVec {bound : Std.PRange.Bound Std.PRange.BoundShape.closed UInt16} {x : BitVec 16} :

Std.PRange.RangeSize.size bound { toBitVec := x } = Std.PRange.RangeSize.size bound.toBitVec x

instance UInt16.instLawfulRangeSizeClosed :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed UInt16

instance UInt16.instRangeSizeOpen :

Std.PRange.RangeSize Std.PRange.BoundShape.open UInt16

Equations

UInt16.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance UInt16.instLawfulRangeSizeOpen :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open UInt16

instance UInt32.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt32

Equations

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

theorem UInt32.succ?_ofBitVec {x : BitVec 32} :

Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt32.succMany?_ofBitVec {k : Nat} {x : BitVec 32} :

Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt32.upwardEnumerableLE_ofBitVec {x y : BitVec 32} :

Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt32.upwardEnumerableLT_ofBitVec {x y : BitVec 32} :

Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt32.instLawfulUpwardEnumerable :

Std.PRange.LawfulUpwardEnumerable UInt32

instance UInt32.instLawfulUpwardEnumerableLE :

Std.PRange.LawfulUpwardEnumerableLE UInt32

instance UInt32.instLawfulOrderLT_1 :

Std.LawfulOrderLT UInt32

instance UInt32.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt32

instance UInt32.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt32

instance UInt32.instLawfulUpwardEnumerableLowerBoundClosed :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed UInt32

instance UInt32.instLawfulUpwardEnumerableUpperBoundClosed :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed UInt32

instance UInt32.instLawfulUpwardEnumerableLowerBoundOpen :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open UInt32

instance UInt32.instLawfulUpwardEnumerableUpperBoundOpen :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open UInt32

instance UInt32.instRangeSizeClosed :

Std.PRange.RangeSize Std.PRange.BoundShape.closed UInt32

Equations

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

theorem UInt32.rangeSizeSize_eq_toBitVec {bound : Std.PRange.Bound Std.PRange.BoundShape.closed UInt32} {x : BitVec 32} :

Std.PRange.RangeSize.size bound { toBitVec := x } = Std.PRange.RangeSize.size bound.toBitVec x

instance UInt32.instLawfulRangeSizeClosed :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed UInt32

instance UInt32.instRangeSizeOpen :

Std.PRange.RangeSize Std.PRange.BoundShape.open UInt32

Equations

UInt32.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance UInt32.instLawfulRangeSizeOpen :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open UInt32

instance UInt64.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt64

Equations

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

theorem UInt64.succ?_ofBitVec {x : BitVec 64} :

Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt64.succMany?_ofBitVec {k : Nat} {x : BitVec 64} :

Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt64.upwardEnumerableLE_ofBitVec {x y : BitVec 64} :

Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt64.upwardEnumerableLT_ofBitVec {x y : BitVec 64} :

Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt64.instLawfulUpwardEnumerable :

Std.PRange.LawfulUpwardEnumerable UInt64

instance UInt64.instLawfulUpwardEnumerableLE :

Std.PRange.LawfulUpwardEnumerableLE UInt64

instance UInt64.instLawfulOrderLT_1 :

Std.LawfulOrderLT UInt64

instance UInt64.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt64

instance UInt64.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt64

instance UInt64.instLawfulUpwardEnumerableLowerBoundClosed :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed UInt64

instance UInt64.instLawfulUpwardEnumerableUpperBoundClosed :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed UInt64

instance UInt64.instLawfulUpwardEnumerableLowerBoundOpen :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open UInt64

instance UInt64.instLawfulUpwardEnumerableUpperBoundOpen :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open UInt64

instance UInt64.instRangeSizeClosed :

Std.PRange.RangeSize Std.PRange.BoundShape.closed UInt64

Equations

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

theorem UInt64.rangeSizeSize_eq_toBitVec {bound : Std.PRange.Bound Std.PRange.BoundShape.closed UInt64} {x : BitVec 64} :

Std.PRange.RangeSize.size bound { toBitVec := x } = Std.PRange.RangeSize.size bound.toBitVec x

instance UInt64.instLawfulRangeSizeClosed :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed UInt64

instance UInt64.instRangeSizeOpen :

Std.PRange.RangeSize Std.PRange.BoundShape.open UInt64

Equations

UInt64.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance UInt64.instLawfulRangeSizeOpen :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open UInt64

instance USize.instUpwardEnumerable :

Std.PRange.UpwardEnumerable USize

Equations

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

theorem USize.succ?_ofBitVec {x : BitVec System.Platform.numBits} :

Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem USize.succMany?_ofBitVec {k : Nat} {x : BitVec System.Platform.numBits} :

Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem USize.upwardEnumerableLE_ofBitVec {x y : BitVec System.Platform.numBits} :

Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem USize.upwardEnumerableLT_ofBitVec {x y : BitVec System.Platform.numBits} :

Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance USize.instLawfulUpwardEnumerable :

Std.PRange.LawfulUpwardEnumerable USize

instance USize.instLawfulUpwardEnumerableLE :

Std.PRange.LawfulUpwardEnumerableLE USize

instance USize.instLawfulOrderLT_1 :

Std.LawfulOrderLT USize

instance USize.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT USize

instance USize.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT USize

instance USize.instLawfulUpwardEnumerableLowerBoundClosed :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.closed USize

instance USize.instLawfulUpwardEnumerableUpperBoundClosed :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.closed USize

instance USize.instLawfulUpwardEnumerableLowerBoundOpen :

Std.PRange.LawfulUpwardEnumerableLowerBound Std.PRange.BoundShape.open USize

instance USize.instLawfulUpwardEnumerableUpperBoundOpen :

Std.PRange.LawfulUpwardEnumerableUpperBound Std.PRange.BoundShape.open USize

instance USize.instRangeSizeClosed :

Std.PRange.RangeSize Std.PRange.BoundShape.closed USize

Equations

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

theorem USize.rangeSizeSize_eq_toBitVec {bound : Std.PRange.Bound Std.PRange.BoundShape.closed USize} {x : BitVec System.Platform.numBits} :

Std.PRange.RangeSize.size bound { toBitVec := x } = Std.PRange.RangeSize.size bound.toBitVec x

instance USize.instLawfulRangeSizeClosed :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.closed USize

instance USize.instRangeSizeOpen :

Std.PRange.RangeSize Std.PRange.BoundShape.open USize

Equations

USize.instRangeSizeOpen = Std.PRange.RangeSize.openOfClosed

instance USize.instLawfulRangeSizeOpen :

Std.PRange.LawfulRangeSize Std.PRange.BoundShape.open USize