The following lemmas are stated purely in terms of `BitVec n`. Their assumptions and statements may seem technical, but they are exactly what is needed in the actual proofs.

source
instance Int8.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Int8
Equations

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

source
instance Int8.instRxcHasSize :
Std.Rxc.HasSize Int8
Equations

- Int8.instRxcHasSize = { size := fun (lo hi : Int8) => (hi.toInt + 1 - lo.toInt).toNat }

source
instance Int8.instRxcLawfulHasSize :
Std.Rxc.LawfulHasSize Int8
source
instance Int8.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite Int8
source
instance Int8.instRxoHasSize :
Std.Rxo.HasSize Int8
Equations

- Int8.instRxoHasSize = Std.Rxo.HasSize.ofClosed

source
instance Int8.instRxoLawfulHasSize :
Std.Rxo.LawfulHasSize Int8
source
instance Int8.instRxoIsAlwaysFinite :
Std.Rxo.IsAlwaysFinite Int8
source
instance Int8.instRxiHasSize :
Std.Rxi.HasSize Int8
Equations

- Int8.instRxiHasSize = { size := fun (lo : Int8) => (2 ^ 7 - lo.toInt).toNat }

source
instance Int8.instRxiLawfulHasSize :
Std.Rxi.LawfulHasSize Int8
source
instance Int8.instRxiIsAlwaysFinite :
Std.Rxi.IsAlwaysFinite Int8
source
instance Int16.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Int16
Equations

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

source
instance Int16.instRxcHasSize :
Std.Rxc.HasSize Int16
Equations

- Int16.instRxcHasSize = { size := fun (lo hi : Int16) => (hi.toInt + 1 - lo.toInt).toNat }

source
instance Int16.instRxcLawfulHasSize :
Std.Rxc.LawfulHasSize Int16
source
instance Int16.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite Int16
source
instance Int16.instRxoHasSize :
Std.Rxo.HasSize Int16
Equations

- Int16.instRxoHasSize = Std.Rxo.HasSize.ofClosed

source
instance Int16.instRxoLawfulHasSize :
Std.Rxo.LawfulHasSize Int16
source
instance Int16.instRxoIsAlwaysFinite :
Std.Rxo.IsAlwaysFinite Int16
source
instance Int16.instRxiHasSize :
Std.Rxi.HasSize Int16
Equations

- Int16.instRxiHasSize = { size := fun (lo : Int16) => (2 ^ 15 - lo.toInt).toNat }

source
instance Int16.instRxiLawfulHasSize :
Std.Rxi.LawfulHasSize Int16
source
instance Int16.instRxiIsAlwaysFinite :
Std.Rxi.IsAlwaysFinite Int16
source
instance Int32.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Int32
Equations

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

source
instance Int32.instRxcHasSize :
Std.Rxc.HasSize Int32
Equations

- Int32.instRxcHasSize = { size := fun (lo hi : Int32) => (hi.toInt + 1 - lo.toInt).toNat }

source
instance Int32.instRxcLawfulHasSize :
Std.Rxc.LawfulHasSize Int32
source
instance Int32.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite Int32
source
instance Int32.instRxoHasSize :
Std.Rxo.HasSize Int32
Equations

- Int32.instRxoHasSize = Std.Rxo.HasSize.ofClosed

source
instance Int32.instRxoLawfulHasSize :
Std.Rxo.LawfulHasSize Int32
source
instance Int32.instRxoIsAlwaysFinite :
Std.Rxo.IsAlwaysFinite Int32
source
instance Int32.instRxiHasSize :
Std.Rxi.HasSize Int32
Equations

- Int32.instRxiHasSize = { size := fun (lo : Int32) => (2 ^ 31 - lo.toInt).toNat }

source
instance Int32.instRxiLawfulHasSize :
Std.Rxi.LawfulHasSize Int32
source
instance Int32.instRxiIsAlwaysFinite :
Std.Rxi.IsAlwaysFinite Int32
source
instance Int64.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Int64
Equations

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

source
instance Int64.instRxcHasSize :
Std.Rxc.HasSize Int64
Equations

- Int64.instRxcHasSize = { size := fun (lo hi : Int64) => (hi.toInt + 1 - lo.toInt).toNat }

source
instance Int64.instRxcLawfulHasSize :
Std.Rxc.LawfulHasSize Int64
source
instance Int64.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite Int64
source
instance Int64.instRxoHasSize :
Std.Rxo.HasSize Int64
Equations

- Int64.instRxoHasSize = Std.Rxo.HasSize.ofClosed

source
instance Int64.instRxoLawfulHasSize :
Std.Rxo.LawfulHasSize Int64
source
instance Int64.instRxoIsAlwaysFinite :
Std.Rxo.IsAlwaysFinite Int64
source
instance Int64.instRxiHasSize :
Std.Rxi.HasSize Int64
Equations

- Int64.instRxiHasSize = { size := fun (lo : Int64) => (2 ^ 63 - lo.toInt).toNat }

source
instance Int64.instRxiLawfulHasSize :
Std.Rxi.LawfulHasSize Int64
source
instance Int64.instRxiIsAlwaysFinite :
Std.Rxi.IsAlwaysFinite Int64
source
instance ISize.instUpwardEnumerable :
Std.PRange.UpwardEnumerable ISize
Equations

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

source
instance ISize.instRxcHasSize :
Std.Rxc.HasSize ISize
Equations

- ISize.instRxcHasSize = { size := fun (lo hi : ISize) => (hi.toInt + 1 - lo.toInt).toNat }

source
instance ISize.instRxcLawfulHasSize :
Std.Rxc.LawfulHasSize ISize
source
instance ISize.instIsAlwaysFinite :
Std.Rxc.IsAlwaysFinite ISize
source
instance ISize.instRxoHasSize :
Std.Rxo.HasSize ISize
Equations

- ISize.instRxoHasSize = Std.Rxo.HasSize.ofClosed

source
instance ISize.instRxoLawfulHasSize :
Std.Rxo.LawfulHasSize ISize
source
instance ISize.instRxoIsAlwaysFinite :
Std.Rxo.IsAlwaysFinite ISize
source
instance ISize.instRxiHasSize :
Std.Rxi.HasSize ISize
Equations

- ISize.instRxiHasSize = { size := fun (lo : ISize) => (2 ^ (System.Platform.numBits - 1) - lo.toInt).toNat }

source
instance ISize.instRxiLawfulHasSize :
Std.Rxi.LawfulHasSize ISize
source
instance ISize.instRxiIsAlwaysFinite :
Std.Rxi.IsAlwaysFinite ISize