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.

instance UInt8.instLeast? :

Std.PRange.Least? UInt8

Equations

UInt8.instLeast? = { least? := some 0 }

instance UInt8.instLawfulUpwardEnumerableLeast? :

Std.PRange.LawfulUpwardEnumerableLeast? UInt8

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.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt8

instance UInt8.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt8

instance UInt8.instHasSize :

Std.Rxc.HasSize UInt8

Equations

UInt8.instHasSize = { size := fun (lo hi : UInt8) => hi.toNat + 1 - lo.toNat }

theorem UInt8.rxcHasSize_eq_toBitVec {lo : BitVec 8} {hi : UInt8} :

Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt8.instLawfulHasSize :

Std.Rxc.LawfulHasSize UInt8

instance UInt8.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite UInt8

instance UInt8.instHasSize_1 :

Std.Rxo.HasSize UInt8

Equations

UInt8.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt8.instLawfulHasSize_1 :

Std.Rxo.LawfulHasSize UInt8

instance UInt8.instIsAlwaysFinite_1 :

Std.Rxo.IsAlwaysFinite UInt8

instance UInt8.instHasSize_2 :

Std.Rxi.HasSize UInt8

Equations

UInt8.instHasSize_2 = { size := fun (lo : UInt8) => 2 ^ 8 - lo.toNat }

theorem UInt8.rxiHasSize_eq_toBitVec {lo : BitVec 8} :

Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt8.instLawfulHasSize_2 :

Std.Rxi.LawfulHasSize UInt8

instance UInt16.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt16

Equations

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

instance UInt16.instLeast? :

Std.PRange.Least? UInt16

Equations

UInt16.instLeast? = { least? := some 0 }

instance UInt16.instLawfulUpwardEnumerableLeast? :

Std.PRange.LawfulUpwardEnumerableLeast? UInt16

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.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt16

instance UInt16.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt16

instance UInt16.instHasSize :

Std.Rxc.HasSize UInt16

Equations

UInt16.instHasSize = { size := fun (lo hi : UInt16) => hi.toNat + 1 - lo.toNat }

theorem UInt16.rxcHasSize_eq_toBitVec {lo : BitVec 16} {hi : UInt16} :

Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt16.instLawfulHasSize :

Std.Rxc.LawfulHasSize UInt16

instance UInt16.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite UInt16

instance UInt16.instHasSize_1 :

Std.Rxo.HasSize UInt16

Equations

UInt16.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt16.instLawfulHasSize_1 :

Std.Rxo.LawfulHasSize UInt16

instance UInt16.instIsAlwaysFinite_1 :

Std.Rxo.IsAlwaysFinite UInt16

instance UInt16.instHasSize_2 :

Std.Rxi.HasSize UInt16

Equations

UInt16.instHasSize_2 = { size := fun (lo : UInt16) => 2 ^ 16 - lo.toNat }

theorem UInt16.rxiHasSize_eq_toBitVec {lo : BitVec 16} :

Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt16.instLawfulHasSize_2 :

Std.Rxi.LawfulHasSize UInt16

instance UInt32.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt32

Equations

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

instance UInt32.instLeast? :

Std.PRange.Least? UInt32

Equations

UInt32.instLeast? = { least? := some 0 }

instance UInt32.instLawfulUpwardEnumerableLeast? :

Std.PRange.LawfulUpwardEnumerableLeast? UInt32

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.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt32

instance UInt32.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt32

instance UInt32.instHasSize :

Std.Rxc.HasSize UInt32

Equations

UInt32.instHasSize = { size := fun (lo hi : UInt32) => hi.toNat + 1 - lo.toNat }

theorem UInt32.rxcHasSize_eq_toBitVec {lo : BitVec 32} {hi : UInt32} :

Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt32.instLawfulHasSize :

Std.Rxc.LawfulHasSize UInt32

instance UInt32.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite UInt32

instance UInt32.instHasSize_1 :

Std.Rxo.HasSize UInt32

Equations

UInt32.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt32.instLawfulHasSize_1 :

Std.Rxo.LawfulHasSize UInt32

instance UInt32.instIsAlwaysFinite_1 :

Std.Rxo.IsAlwaysFinite UInt32

instance UInt32.instHasSize_2 :

Std.Rxi.HasSize UInt32

Equations

UInt32.instHasSize_2 = { size := fun (lo : UInt32) => 2 ^ 32 - lo.toNat }

theorem UInt32.rxiHasSize_eq_toBitVec {lo : BitVec 32} :

Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt32.instLawfulHasSize_2 :

Std.Rxi.LawfulHasSize UInt32

instance UInt64.instUpwardEnumerable :

Std.PRange.UpwardEnumerable UInt64

Equations

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

instance UInt64.instLeast? :

Std.PRange.Least? UInt64

Equations

UInt64.instLeast? = { least? := some 0 }

instance UInt64.instLawfulUpwardEnumerableLeast? :

Std.PRange.LawfulUpwardEnumerableLeast? UInt64

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.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT UInt64

instance UInt64.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT UInt64

instance UInt64.instHasSize :

Std.Rxc.HasSize UInt64

Equations

UInt64.instHasSize = { size := fun (lo hi : UInt64) => hi.toNat + 1 - lo.toNat }

theorem UInt64.rxcHasSize_eq_toBitVec {lo : BitVec 64} {hi : UInt64} :

Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt64.instLawfulHasSize :

Std.Rxc.LawfulHasSize UInt64

instance UInt64.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite UInt64

instance UInt64.instHasSize_1 :

Std.Rxo.HasSize UInt64

Equations

UInt64.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt64.instLawfulHasSize_1 :

Std.Rxo.LawfulHasSize UInt64

instance UInt64.instIsAlwaysFinite_1 :

Std.Rxo.IsAlwaysFinite UInt64

instance UInt64.instHasSize_2 :

Std.Rxi.HasSize UInt64

Equations

UInt64.instHasSize_2 = { size := fun (lo : UInt64) => 2 ^ 64 - lo.toNat }

theorem UInt64.rxiHasSize_eq_toBitVec {lo : BitVec 64} :

Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt64.instLawfulHasSize_2 :

Std.Rxi.LawfulHasSize UInt64

instance USize.instUpwardEnumerable :

Std.PRange.UpwardEnumerable USize

Equations

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

instance USize.instLeast? :

Std.PRange.Least? USize

Equations

USize.instLeast? = { least? := some 0 }

instance USize.instLawfulUpwardEnumerableLeast? :

Std.PRange.LawfulUpwardEnumerableLeast? USize

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.instLawfulUpwardEnumerableLT :

Std.PRange.LawfulUpwardEnumerableLT USize

instance USize.instLawfulUpwardEnumerableLT_1 :

Std.PRange.LawfulUpwardEnumerableLT USize

instance USize.instHasSize :

Std.Rxc.HasSize USize

Equations

USize.instHasSize = { size := fun (lo hi : USize) => hi.toNat + 1 - lo.toNat }

theorem USize.rxcHasSize_eq_toBitVec {lo : BitVec System.Platform.numBits} {hi : USize} :

Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance USize.instLawfulHasSize :

Std.Rxc.LawfulHasSize USize

instance USize.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite USize

instance USize.instHasSize_1 :

Std.Rxo.HasSize USize

Equations

USize.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance USize.instLawfulHasSize_1 :

Std.Rxo.LawfulHasSize USize

instance USize.instIsAlwaysFinite_1 :

Std.Rxo.IsAlwaysFinite USize

instance USize.instHasSize_2 :

Std.Rxi.HasSize USize

Equations

USize.instHasSize_2 = { size := fun (lo : USize) => 2 ^ System.Platform.numBits - lo.toNat }

theorem USize.rxiHasSize_eq_toBitVec {lo : BitVec System.Platform.numBits} :

Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance USize.instLawfulHasSize_2 :

Std.Rxi.LawfulHasSize USize