TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Formatting

External character output for configured binary values #

Storage selection affects neither the characters nor the exception indicators. The descriptor model supplies the shortest, exact, significant-digit, fixed, scientific and hexadecimal algorithms.

source
@[inline]
def FloatLib.Floats.ExecFloat.Binary.format {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Binary fmt.expWidth fmt.fracWidth fmt.encoding fmt.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (style : Formats.BinaryInterchange.Model.TextStyle := Formats.BinaryInterchange.Model.TextStyle.shortest) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) :
match status with | true => Formats.BinaryInterchange.Model.TextOutcome | false => String

Write a configured value as text, as Model.format: by default the shortest decimal that reads back as value (what toString and #eval show), otherwise in style with rounding in mode and, with status := true, the inexact indicator.

Instances For
    source
    @[simp]
    theorem FloatLib.Floats.ExecFloat.Binary.format_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Formats.BinaryInterchange.Model fmt) (style : Formats.BinaryInterchange.Model.TextStyle) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) (status : Bool) :
    (ofModel value).format style mode status = value.format style mode status

    Text and its status are independent of the storage representation.