TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Info

Format inspection #

#float_info reports a numerical type's format, backends, and available theorems. #float_info! includes theorem names and hypotheses; #float_help lists the command options.

Info.Profile defines report data and checks theorem references. Info.Inspection discovers capabilities and backend metadata, Info.Render formats the report, and Info.Command defines the syntax. Format families register renderers in their own Info modules.

source
def FloatLib.Floats.ExecFloat.Inspection.renderProfile (profile : FormatProfile) (valueType : Lean.Expr) (operations : CoreOperationCoverage) :
Lean.MetaM String

Attach conversion capabilities discovered for a value type, validate the declarations relevant to the report mode, and render the profile. Format modules supply representation and semantics.

Instances For
    source
    def FloatLib.Floats.ExecFloat.Inspection.renderExecProfile (profile : FormatProfile) (valueType family : Lean.Expr) :
    Lean.MetaM String

    Render a profile using the universal operations actually installed for an ExecFloat family.

    Instances For