instance Trestle.instIndexTypeBool : IndexType Bool

Equations

• Trestle.instIndexTypeBool = Trestle.IndexType.ofEquiv Bool.proxyTypeEquiv

instance Trestle.instLawfulIndexTypeBool : LawfulIndexType Bool

instance Trestle.instIndexTypeBitVec {w✝ : ℕ} : IndexType (BitVec w✝)

Equations

• Trestle.instIndexTypeBitVec = Trestle.IndexType.ofEquiv (BitVec.proxyTypeEquiv w✝)

instance Trestle.instLawfulIndexTypeBitVec {w✝ : ℕ} : LawfulIndexType (BitVec w✝)

instance Trestle.instLawfulIndexTypeUInt8 : LawfulIndexType UInt8

instance Trestle.instIndexTypeUInt8 : IndexType UInt8

Equations

• Trestle.instIndexTypeUInt8 = Trestle.IndexType.ofEquiv UInt8.proxyTypeEquiv

instance Trestle.instIndexTypeUInt16 : IndexType UInt16

Equations

• Trestle.instIndexTypeUInt16 = Trestle.IndexType.ofEquiv UInt16.proxyTypeEquiv

instance Trestle.instLawfulIndexTypeUInt16 : LawfulIndexType UInt16

instance Trestle.instIndexTypeUInt32 : IndexType UInt32

Equations

• Trestle.instIndexTypeUInt32 = Trestle.IndexType.ofEquiv UInt32.proxyTypeEquiv

instance Trestle.instLawfulIndexTypeUInt32 : LawfulIndexType UInt32

instance Trestle.instLawfulIndexTypeUInt64 : LawfulIndexType UInt64

instance Trestle.instIndexTypeUInt64 : IndexType UInt64

Equations

• Trestle.instIndexTypeUInt64 = Trestle.IndexType.ofEquiv UInt64.proxyTypeEquiv