TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Logarithmic.Configured.Core

Configured exact logarithmic identity #

The encoded logarithmic family supplies the public ExecFloat.Logarithmic type. The representation contains only zero or a sign with an unbounded integer exponent; it does not impose a bit layout.

source
inductive FloatLib.Floats.ExecFloat.Logarithmic.Family (radix : Numerics.Radix) :
Type

Type-level identity of an exact logarithmic format at one radix.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.Logarithmic.instEncodedFormatFamily (radix : Numerics.Radix) :
    Numerics.EncodedFormat (Family radix)
    source
    @[instance_reducible]
    noncomputable instance FloatLib.Floats.ExecFloat.Logarithmic.instFormatSemanticsFamily (radix : Numerics.Radix) :
    Numerics.FormatSemantics (Family radix)
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.ExecFloat.Logarithmic (radix : Numerics.Radix) :
    Type

    Exact zero and signed integral powers of radix, using the common ExecFloat carrier.

    Instances For