Widget Gallery

This file is best explored in an editor:

• put the cursor on a #tensor_view / #ir_view / #float32_view line, and
• Lean will render a small interactive HTML panel in the infoview.

These widgets are inspection tools for teaching, debugging, and reviewing artifacts without leaving Lean. They are intentionally available through the dedicated widget entrypoint (import NN.Entrypoint.Widgets) so ordinary runtime and proof imports stay lightweight.

RL (GridWorld) widgets

These small panels are useful when iterating on RL specs and proofs: they let you quickly sanity-check state encodings, policies, and rollout traces in the infoview.

Actual training curve (SGD on a small regression dataset).

This is a real “training loop” computed in Lean. It is intentionally compact (2→2→1 MLP) so the widget evaluator can run it quickly inside the editor.

Note: We keep this example self-contained (no Spec-tensor forward/backward), because the full spec-side MLP backprop pipeline is large and would make this widget file slow to elaborate.

Tensor basics / bridge example:

Widgets are defined for Spec.Tensor (shape-indexed, spec-level tensors). If you have an array-backed TensorArray.Tensor (common at IO boundaries), you can convert it with TensorBridge.to_tensor and then use the same #tensor_view UI.