Formatting inspection reports

Compact and detailed reports from FormatProfile data and discovered operation capabilities. Family profiles supply theorem references and hypothesis summaries; declaration validation checks that the referenced names exist with the required kind. Both report styles use the same data.

def FloatLib.Floats.ExecFloat.Internal.renderEntries (title : String) (entries : List InfoEntry) : String

Render one section of labeled report entries.

def FloatLib.Floats.ExecFloat.Internal.renderEntriesCompact (title : String) (entries : List InfoEntry) (limit : Nat) : String

Render a bounded section and direct users to the detailed report for the remainder.

def FloatLib.Floats.ExecFloat.Internal.renderCapability (name : String) (available : Bool) : String

Render one proof-backed capability status.

def FloatLib.Floats.ExecFloat.Internal.renderCoreOperations (coverage : CoreOperationCoverage) : String

Render proof-backed coverage of the universal arithmetic operations.

def FloatLib.Floats.ExecFloat.Internal.renderSpecializedOperations (operations : List InfoEntry) : String

Render executable APIs that intentionally live outside the universal scalar interface.

def FloatLib.Floats.ExecFloat.Internal.renderApplicability : TheoremApplicability → String

Render descriptor-level theorem applicability.

def FloatLib.Floats.ExecFloat.Internal.renderTheoremSurface (declarationPrefix : String) (surface : TheoremSurface) : String

Render one semantic theorem group, its applicability, and its remaining scope.

def FloatLib.Floats.ExecFloat.Internal.renderTheoremSurfaces (declarationPrefix : String) (surfaces : List TheoremSurface) : String

Render all semantic theorem groups in a profile.

def FloatLib.Floats.ExecFloat.Internal.renderNonclaims (nonclaims : List String) : String

Render the explicit limits of the report's proof boundary.

def FloatLib.Floats.ExecFloat.Internal.renderNumericalAnalysisKind : NumericalAnalysisKind → String

Render a numerical-analysis category in ordinary numerical language.

def FloatLib.Floats.ExecFloat.Internal.renderNumericalGuarantee (declarationPrefix : String) (surface : TheoremSurface) (guarantee : NumericalGuarantee) : String

Render one checked range, roundoff, or exactness contract.

def FloatLib.Floats.ExecFloat.Internal.renderNumericalGuaranteeCompact (surface : TheoremSurface) (guarantee : NumericalGuarantee) : String

Render one numerical contract without the declaration inventory or full hypothesis text.

def FloatLib.Floats.ExecFloat.Internal.renderNumericalAnalysis (profile : FormatProfile) (detailed : Bool) : String

Render only numerical-analysis contracts explicitly registered by a format profile.

This mode reports type-level theorem surfaces. An expression-level bound additionally needs ranges for its inputs and a theorem that composes the operations in the expression.

def FloatLib.Floats.ExecFloat.Internal.renderFormatInfoDetailed (profile : FormatProfile) (coreOperations : CoreOperationCoverage) : String

Render the complete proof and backend audit report.

def FloatLib.Floats.ExecFloat.Internal.renderTheoremSurfaceCompact (surface : TheoremSurface) : String

Render one theorem group as a concise proof-coverage statement.

def FloatLib.Floats.ExecFloat.Internal.renderTheoremSurfacesCompact (surfaces : List TheoremSurface) (limit : Nat := 4) : String

Render the proof topics without flooding the InfoView with declaration inventories.

def FloatLib.Floats.ExecFloat.Internal.renderArithmeticCompact (coverage : CoreOperationCoverage) (specializedOperations : List InfoEntry) : String

Render compact proof-backed coverage of the universal arithmetic interface.

def FloatLib.Floats.ExecFloat.Internal.renderExecutionCompact (entries : List InfoEntry) : String

Render only execution facts useful to a caller choosing or profiling a format.

def FloatLib.Floats.ExecFloat.Internal.renderFormatInfoCompact (profile : FormatProfile) (coreOperations : CoreOperationCoverage) : String

Render the normal, user-facing numerical-format summary.

def FloatLib.Floats.ExecFloat.renderFormatInfo (profile : FormatProfile) (coreOperations : CoreOperationCoverage) : Lean.CoreM String

Render a numerical-format report according to the command option.

Normal #float_info is intentionally concise. #float_info! enables the complete theorem and backend audit without maintaining a second family-specific inspector.