Format inspection commands

Syntax and elaboration for #float_help, #float_info, and #float_info!. Each format package registers a renderer for its configured types. The final rule reports an unsupported type when no renderer recognizes it.

Commands inspect elaborated types at compile time. Adding a format renderer requires no change to arithmetic execution.

def floatHelpCmd : Lean.ParserDescr

Print a short guide to configuring numerical types, inspecting their semantics, and finding the family entry points.

def floatInfoCmd : Lean.ParserDescr

Print the format, value classes, execution strategy, proof-backed operation coverage, semantic theorem groups, and documented proof limits for an executable numerical type.

def floatInfoErrorsCmd : Lean.ParserDescr

Focus the report on checked range, roundoff, and exactness contracts.

def floatInfoDetailedCmd : Lean.ParserDescr

Print the full report: theorems, backend planning, and the trust boundary.

def floatInfoErrorsDetailedCmd : Lean.ParserDescr

Show the detailed theorem inventory for numerical-analysis contracts only.

def FloatLib.Floats.ExecFloat.FloatInfo.Command.elaborateType (type : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Elaborate and fully instantiate the numerical type supplied to #float_info.

Every family renderer reaches it through withElaboratedType.

def FloatLib.Floats.ExecFloat.FloatInfo.Command.withElaboratedType (type : Lean.Syntax) (render : Lean.Expr → Lean.Elab.TermElabM Unit) : Lean.Elab.Command.CommandElabM Unit

Run one family renderer on a fully elaborated type without modifying the environment.

Every #float_info extension goes through this one command-elaboration boundary.

def FloatLib.Floats.ExecFloat.FloatInfo.Command.withExecFamilyApplication (type : Lean.Syntax) (familyName : Lean.Name) (arity : ℕ) (render : Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM Unit) : Lean.Elab.Command.CommandElabM Unit

Run a #float_info renderer when the supplied type is an ExecFloat family built by familyName with arity arguments.

A mismatch raises unsupportedSyntax, so Lean tries the next registered format renderer. The callback receives the value type, the recovered family, and the family arguments.