TorchLean API

FloatLib.Floats.Formats.Posit.Configured.Storage.Native.Instances

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)