Inspecting proof-carrying capabilities and backend plans

Capability inspection reads the instances that execution uses. It reports the installed conversions, which universal operations exist, the candidate selected by each capability, and the planner decisions behind that selection. The selected candidate comes from the capability itself. Diagnostic assessments rerun the shared selector on the capability's candidate estimates and policy.

def FloatLib.Floats.ExecFloat.Inspection.conversions (valueType : Lean.Expr) : Lean.MetaM (List InfoEntry)

Inspect the explicit conversion capabilities installed for one value type.

Source decoding, destination quantization, and a default context are inspected independently. A source-only family can supply operands to casts or mixed arithmetic. A destination without a default context needs a (context := ...) argument.

def FloatLib.Floats.ExecFloat.Inspection.withConversions (profile : FormatProfile) (valueType : Lean.Expr) : Lean.MetaM FormatProfile

Attach synthesized conversion capabilities to a family-authored format profile.

def FloatLib.Floats.ExecFloat.Inspection.execFamily? (valueType : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Recover the configured family encoded by an ExecFloat value type.

The check recognizes a Subtype predicate of the form fun _ => ExecFloatTag family. It recovers the tag without checking that the underlying carrier is the code type of family.

def FloatLib.Floats.ExecFloat.Inspection.execFamilyApplication? (familyName : Lean.Name) (arity : ℕ) (valueType : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))

Recover an ExecFloat family that is an application of familyName to arity arguments, together with those arguments. The returned array is safe to index below arity.

def FloatLib.Floats.ExecFloat.Inspection.hasCapability (className : Lean.Name) (family : Lean.Expr) : Lean.MetaM Bool

Whether family has EncodedFormat, Backend.PolicyFor, and className instances.

Availability comes from instance synthesis, never from declaration names or storage widths.

def FloatLib.Floats.ExecFloat.Inspection.coreOperations (family : Lean.Expr) : Lean.MetaM CoreOperationCoverage

Inspect all six universal operation capabilities for one configured family.

def FloatLib.Floats.ExecFloat.Inspection.reduceProjection (fieldName : Lean.Name) (object : Lean.Expr) : Lean.MetaM Lean.Expr

Reduce the projection fieldName of a closed expression at full transparency.

Format-specific #float_info elaborators use it to inspect embedded descriptors.

def FloatLib.Floats.ExecFloat.Inspection.readFlagProjection (description : String) (fieldName trueConstructor falseConstructor : Lean.Name) (object : Lean.Expr) : Lean.MetaM Bool

Read a closed two-constructor projection as a Boolean report field.

The caller names the constructors that mean true and false. The reduced value is compared with those constructor names, never with printed names or constructor order.

def FloatLib.Floats.ExecFloat.Inspection.readNat (description : String) (value : Lean.Expr) : Lean.MetaM ℕ

Read a closed natural-number expression after reduction.

Family-specific #float_info elaborators use it for static widths, radix bases, and scale parameters, so every family shares one reduction and one error message.

def FloatLib.Floats.ExecFloat.Inspection.readNatProjection (description : String) (fieldName : Lean.Name) (object : Lean.Expr) : Lean.MetaM ℕ

Read a natural-number-valued projection from a closed expression.

The error message names the embedded descriptor or plan by description and the field that failed to reduce by fieldName.

def FloatLib.Floats.ExecFloat.Inspection.readString (description : String) (value : Lean.Expr) : Lean.MetaM String

Evaluate one closed string expression.

def FloatLib.Floats.ExecFloat.Inspection.selectedBackends (family : Lean.Expr) : Lean.MetaM (List InfoEntry)

Report the selected backend and every alternative for each synthesized universal capability.

Families append these entries to their own execution profile, so selection reports look the same across families without imposing a common numerical model.