Native-word instances for configured posit carriers #
The four primitive storage plans implement the direct UInt64 capability. Each conversion is
proved exact from the plan's static width bound.
@[instance_reducible]
instance
FloatLib.Floats.Formats.Posit.Configured.byteNativeCode
(format : Format)
(width_le : format.bits ≤ 8)
:
NativeCode format (StoragePlan.byte width_le)
@[instance_reducible]
instance
FloatLib.Floats.Formats.Posit.Configured.word16NativeCode
(format : Format)
(width_le : format.bits ≤ 16)
:
NativeCode format (StoragePlan.word16 width_le)
@[instance_reducible]
instance
FloatLib.Floats.Formats.Posit.Configured.word32NativeCode
(format : Format)
(width_le : format.bits ≤ 32)
:
NativeCode format (StoragePlan.word32 width_le)
@[instance_reducible]
instance
FloatLib.Floats.Formats.Posit.Configured.word64NativeCode
(format : Format)
(width_le : format.bits ≤ 64)
:
NativeCode format (StoragePlan.word64 width_le)