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 concise guide to configuring numerical types, inspecting their semantics, and finding the family-specific constructors exported by the currently imported FloatLib package.

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

Enable the complete theorem, backend-planning, and trust-boundary audit report.

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 uses this same command boundary before inspecting its carrier shape.

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 against a fully elaborated type without mutating the environment.

This keeps every #float_info extension on the same 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 only when the supplied type uses one exact ExecFloat family.

A family mismatch raises unsupportedSyntax, which lets Lean try the next registered format renderer. The callback receives the user-facing value type, the recovered family, and the checked family arguments. Format modules supply their own report data.