Documentation

Init.Data.Range.Polymorphic.SInt

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.

instance Int8.instUpwardEnumerable :

Std.PRange.UpwardEnumerable Int8

Equations

instance Int8.instRxcHasSize :

Std.Rxc.HasSize Int8

Equations

instance Int8.instRxcLawfulHasSize :

Std.Rxc.LawfulHasSize Int8

instance Int8.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite Int8

instance Int8.instRxoHasSize :

Std.Rxo.HasSize Int8

Equations

instance Int8.instRxoLawfulHasSize :

Std.Rxo.LawfulHasSize Int8

instance Int8.instRxoIsAlwaysFinite :

Std.Rxo.IsAlwaysFinite Int8

instance Int8.instRxiHasSize :

Std.Rxi.HasSize Int8

Equations

instance Int8.instRxiLawfulHasSize :

Std.Rxi.LawfulHasSize Int8

instance Int8.instRxiIsAlwaysFinite :

Std.Rxi.IsAlwaysFinite Int8

instance Int16.instUpwardEnumerable :

Std.PRange.UpwardEnumerable Int16

Equations

instance Int16.instRxcHasSize :

Std.Rxc.HasSize Int16

Equations

instance Int16.instRxcLawfulHasSize :

Std.Rxc.LawfulHasSize Int16

instance Int16.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite Int16

instance Int16.instRxoHasSize :

Std.Rxo.HasSize Int16

Equations

instance Int16.instRxoLawfulHasSize :

Std.Rxo.LawfulHasSize Int16

instance Int16.instRxoIsAlwaysFinite :

Std.Rxo.IsAlwaysFinite Int16

instance Int16.instRxiHasSize :

Std.Rxi.HasSize Int16

Equations

instance Int16.instRxiLawfulHasSize :

Std.Rxi.LawfulHasSize Int16

instance Int16.instRxiIsAlwaysFinite :

Std.Rxi.IsAlwaysFinite Int16

instance Int32.instUpwardEnumerable :

Std.PRange.UpwardEnumerable Int32

Equations

instance Int32.instRxcHasSize :

Std.Rxc.HasSize Int32

Equations

instance Int32.instRxcLawfulHasSize :

Std.Rxc.LawfulHasSize Int32

instance Int32.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite Int32

instance Int32.instRxoHasSize :

Std.Rxo.HasSize Int32

Equations

instance Int32.instRxoLawfulHasSize :

Std.Rxo.LawfulHasSize Int32

instance Int32.instRxoIsAlwaysFinite :

Std.Rxo.IsAlwaysFinite Int32

instance Int32.instRxiHasSize :

Std.Rxi.HasSize Int32

Equations

instance Int32.instRxiLawfulHasSize :

Std.Rxi.LawfulHasSize Int32

instance Int32.instRxiIsAlwaysFinite :

Std.Rxi.IsAlwaysFinite Int32

instance Int64.instUpwardEnumerable :

Std.PRange.UpwardEnumerable Int64

Equations

instance Int64.instRxcHasSize :

Std.Rxc.HasSize Int64

Equations

instance Int64.instRxcLawfulHasSize :

Std.Rxc.LawfulHasSize Int64

instance Int64.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite Int64

instance Int64.instRxoHasSize :

Std.Rxo.HasSize Int64

Equations

instance Int64.instRxoLawfulHasSize :

Std.Rxo.LawfulHasSize Int64

instance Int64.instRxoIsAlwaysFinite :

Std.Rxo.IsAlwaysFinite Int64

instance Int64.instRxiHasSize :

Std.Rxi.HasSize Int64

Equations

instance Int64.instRxiLawfulHasSize :

Std.Rxi.LawfulHasSize Int64

instance Int64.instRxiIsAlwaysFinite :

Std.Rxi.IsAlwaysFinite Int64

instance ISize.instUpwardEnumerable :

Std.PRange.UpwardEnumerable ISize

Equations

instance ISize.instRxcHasSize :

Std.Rxc.HasSize ISize

Equations

instance ISize.instRxcLawfulHasSize :

Std.Rxc.LawfulHasSize ISize

instance ISize.instIsAlwaysFinite :

Std.Rxc.IsAlwaysFinite ISize

instance ISize.instRxoHasSize :

Std.Rxo.HasSize ISize

Equations

instance ISize.instRxoLawfulHasSize :

Std.Rxo.LawfulHasSize ISize

instance ISize.instRxoIsAlwaysFinite :

Std.Rxo.IsAlwaysFinite ISize

instance ISize.instRxiHasSize :

Std.Rxi.HasSize ISize

Equations

instance ISize.instRxiLawfulHasSize :

Std.Rxi.LawfulHasSize ISize

instance ISize.instRxiIsAlwaysFinite :

Std.Rxi.IsAlwaysFinite ISize