Documentation

Init.Data.Range.Polymorphic.UInt

source
@[instance_reducible]
instance UInt8.instUpwardEnumerable :
Std.PRange.UpwardEnumerable UInt8
source
@[instance_reducible]
instance UInt8.instLeast? :
Std.PRange.Least? UInt8
source
instance UInt8.instLawfulUpwardEnumerableLeast? :
Std.PRange.LawfulUpwardEnumerableLeast? UInt8
source
theorem UInt8.succ?_ofBitVec {x : BitVec 8} :
Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x
source
theorem UInt8.succMany?_ofBitVec {k : Nat} {x : BitVec 8} :
Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x
source
theorem UInt8.upwardEnumerableLE_ofBitVec {x y : BitVec 8} :
Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
source
theorem UInt8.upwardEnumerableLT_ofBitVec {x y : BitVec 8} :
Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
source
instance UInt8.instLawfulUpwardEnumerable :
Std.PRange.LawfulUpwardEnumerable UInt8
source
instance UInt8.instLawfulUpwardEnumerableLE :
Std.PRange.LawfulUpwardEnumerableLE UInt8
source
instance UInt8.instLawfulUpwardEnumerableLT :
Std.PRange.LawfulUpwardEnumerableLT UInt8
source
@[instance_reducible]
instance UInt8.instHasSize :
Std.Rxc.HasSize UInt8
source
theorem UInt8.rxcHasSize_eq_toBitVec {lo : BitVec 8} {hi : UInt8} :
Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
source
instance UInt8.instLawfulHasSize :
Std.Rxc.LawfulHasSize UInt8
source
instance UInt8.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite UInt8
source
@[instance_reducible]
instance UInt8.instHasSize_1 :
Std.Rxo.HasSize UInt8
source
instance UInt8.instLawfulHasSize_1 :
Std.Rxo.LawfulHasSize UInt8
source
instance UInt8.instIsAlwaysFinite_1 :
Std.Rxo.IsAlwaysFinite UInt8
source
@[instance_reducible]
instance UInt8.instHasSize_2 :
Std.Rxi.HasSize UInt8
source
theorem UInt8.rxiHasSize_eq_toBitVec {lo : BitVec 8} :
Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
source
instance UInt8.instLawfulHasSize_2 :
Std.Rxi.LawfulHasSize UInt8
source
@[instance_reducible]
instance UInt16.instUpwardEnumerable :
Std.PRange.UpwardEnumerable UInt16
source
@[instance_reducible]
instance UInt16.instLeast? :
Std.PRange.Least? UInt16
source
instance UInt16.instLawfulUpwardEnumerableLeast? :
Std.PRange.LawfulUpwardEnumerableLeast? UInt16
source
theorem UInt16.succ?_ofBitVec {x : BitVec 16} :
Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x
source
theorem UInt16.succMany?_ofBitVec {k : Nat} {x : BitVec 16} :
Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x
source
theorem UInt16.upwardEnumerableLE_ofBitVec {x y : BitVec 16} :
Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
source
theorem UInt16.upwardEnumerableLT_ofBitVec {x y : BitVec 16} :
Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
source
instance UInt16.instLawfulUpwardEnumerable :
Std.PRange.LawfulUpwardEnumerable UInt16
source
instance UInt16.instLawfulUpwardEnumerableLE :
Std.PRange.LawfulUpwardEnumerableLE UInt16
source
instance UInt16.instLawfulUpwardEnumerableLT :
Std.PRange.LawfulUpwardEnumerableLT UInt16
source
@[instance_reducible]
instance UInt16.instHasSize :
Std.Rxc.HasSize UInt16
source
theorem UInt16.rxcHasSize_eq_toBitVec {lo : BitVec 16} {hi : UInt16} :
Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
source
instance UInt16.instLawfulHasSize :
Std.Rxc.LawfulHasSize UInt16
source
instance UInt16.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite UInt16
source
@[instance_reducible]
instance UInt16.instHasSize_1 :
Std.Rxo.HasSize UInt16
source
instance UInt16.instLawfulHasSize_1 :
Std.Rxo.LawfulHasSize UInt16
source
instance UInt16.instIsAlwaysFinite_1 :
Std.Rxo.IsAlwaysFinite UInt16
source
@[instance_reducible]
instance UInt16.instHasSize_2 :
Std.Rxi.HasSize UInt16
source
theorem UInt16.rxiHasSize_eq_toBitVec {lo : BitVec 16} :
Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
source
instance UInt16.instLawfulHasSize_2 :
Std.Rxi.LawfulHasSize UInt16
source
@[instance_reducible]
instance UInt32.instUpwardEnumerable :
Std.PRange.UpwardEnumerable UInt32
source
@[instance_reducible]
instance UInt32.instLeast? :
Std.PRange.Least? UInt32
source
instance UInt32.instLawfulUpwardEnumerableLeast? :
Std.PRange.LawfulUpwardEnumerableLeast? UInt32
source
theorem UInt32.succ?_ofBitVec {x : BitVec 32} :
Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x
source
theorem UInt32.succMany?_ofBitVec {k : Nat} {x : BitVec 32} :
Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x
source
theorem UInt32.upwardEnumerableLE_ofBitVec {x y : BitVec 32} :
Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
source
theorem UInt32.upwardEnumerableLT_ofBitVec {x y : BitVec 32} :
Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
source
instance UInt32.instLawfulUpwardEnumerable :
Std.PRange.LawfulUpwardEnumerable UInt32
source
instance UInt32.instLawfulUpwardEnumerableLE :
Std.PRange.LawfulUpwardEnumerableLE UInt32
source
instance UInt32.instLawfulUpwardEnumerableLT :
Std.PRange.LawfulUpwardEnumerableLT UInt32
source
@[instance_reducible]
instance UInt32.instHasSize :
Std.Rxc.HasSize UInt32
source
theorem UInt32.rxcHasSize_eq_toBitVec {lo : BitVec 32} {hi : UInt32} :
Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
source
instance UInt32.instLawfulHasSize :
Std.Rxc.LawfulHasSize UInt32
source
instance UInt32.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite UInt32
source
@[instance_reducible]
instance UInt32.instHasSize_1 :
Std.Rxo.HasSize UInt32
source
instance UInt32.instLawfulHasSize_1 :
Std.Rxo.LawfulHasSize UInt32
source
instance UInt32.instIsAlwaysFinite_1 :
Std.Rxo.IsAlwaysFinite UInt32
source
@[instance_reducible]
instance UInt32.instHasSize_2 :
Std.Rxi.HasSize UInt32
source
theorem UInt32.rxiHasSize_eq_toBitVec {lo : BitVec 32} :
Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
source
instance UInt32.instLawfulHasSize_2 :
Std.Rxi.LawfulHasSize UInt32
source
@[instance_reducible]
instance UInt64.instUpwardEnumerable :
Std.PRange.UpwardEnumerable UInt64
source
@[instance_reducible]
instance UInt64.instLeast? :
Std.PRange.Least? UInt64
source
instance UInt64.instLawfulUpwardEnumerableLeast? :
Std.PRange.LawfulUpwardEnumerableLeast? UInt64
source
theorem UInt64.succ?_ofBitVec {x : BitVec 64} :
Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x
source
theorem UInt64.succMany?_ofBitVec {k : Nat} {x : BitVec 64} :
Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x
source
theorem UInt64.upwardEnumerableLE_ofBitVec {x y : BitVec 64} :
Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
source
theorem UInt64.upwardEnumerableLT_ofBitVec {x y : BitVec 64} :
Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
source
instance UInt64.instLawfulUpwardEnumerable :
Std.PRange.LawfulUpwardEnumerable UInt64
source
instance UInt64.instLawfulUpwardEnumerableLE :
Std.PRange.LawfulUpwardEnumerableLE UInt64
source
instance UInt64.instLawfulUpwardEnumerableLT :
Std.PRange.LawfulUpwardEnumerableLT UInt64
source
@[instance_reducible]
instance UInt64.instHasSize :
Std.Rxc.HasSize UInt64
source
theorem UInt64.rxcHasSize_eq_toBitVec {lo : BitVec 64} {hi : UInt64} :
Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
source
instance UInt64.instLawfulHasSize :
Std.Rxc.LawfulHasSize UInt64
source
instance UInt64.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite UInt64
source
@[instance_reducible]
instance UInt64.instHasSize_1 :
Std.Rxo.HasSize UInt64
source
instance UInt64.instLawfulHasSize_1 :
Std.Rxo.LawfulHasSize UInt64
source
instance UInt64.instIsAlwaysFinite_1 :
Std.Rxo.IsAlwaysFinite UInt64
source
@[instance_reducible]
instance UInt64.instHasSize_2 :
Std.Rxi.HasSize UInt64
source
theorem UInt64.rxiHasSize_eq_toBitVec {lo : BitVec 64} :
Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
source
instance UInt64.instLawfulHasSize_2 :
Std.Rxi.LawfulHasSize UInt64
source
@[instance_reducible]
instance USize.instUpwardEnumerable :
Std.PRange.UpwardEnumerable USize
source
@[instance_reducible]
instance USize.instLeast? :
Std.PRange.Least? USize
source
instance USize.instLawfulUpwardEnumerableLeast? :
Std.PRange.LawfulUpwardEnumerableLeast? USize
source
theorem USize.succ?_ofBitVec {x : BitVec System.Platform.numBits} :
Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x
source
theorem USize.succMany?_ofBitVec {k : Nat} {x : BitVec System.Platform.numBits} :
Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x
source
theorem USize.upwardEnumerableLE_ofBitVec {x y : BitVec System.Platform.numBits} :
Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
source
theorem USize.upwardEnumerableLT_ofBitVec {x y : BitVec System.Platform.numBits} :
Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
source
instance USize.instLawfulUpwardEnumerable :
Std.PRange.LawfulUpwardEnumerable USize
source
instance USize.instLawfulUpwardEnumerableLE :
Std.PRange.LawfulUpwardEnumerableLE USize
source
instance USize.instLawfulUpwardEnumerableLT :
Std.PRange.LawfulUpwardEnumerableLT USize
source
@[instance_reducible]
instance USize.instHasSize :
Std.Rxc.HasSize USize
source
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
source
instance USize.instLawfulHasSize :
Std.Rxc.LawfulHasSize USize
source
instance USize.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite USize
source
@[instance_reducible]
instance USize.instHasSize_1 :
Std.Rxo.HasSize USize
source
instance USize.instLawfulHasSize_1 :
Std.Rxo.LawfulHasSize USize
source
instance USize.instIsAlwaysFinite_1 :
Std.Rxo.IsAlwaysFinite USize
source
@[instance_reducible]
instance USize.instHasSize_2 :
Std.Rxi.HasSize USize
source
theorem USize.rxiHasSize_eq_toBitVec {lo : BitVec System.Platform.numBits} :
Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo
source
instance USize.instLawfulHasSize_2 :
Std.Rxi.LawfulHasSize USize