Widget Gallery

The gallery 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 available through the dedicated widget entrypoint (import NN.Entrypoint.Widgets) so ordinary runtime and proof imports stay focused.

RL (GridWorld) widgets

These compact panels are useful when iterating on RL specs and proofs: they let you inspect 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. The model is compact (2→2→1 MLP), which keeps the widget responsive 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.