Quickstart: Widgets

TorchLean widgets are editor-side inspection tools. They are not part of the runtime semantics and they do not change proofs; they simply render the values you already have in Lean.

Use this file in the editor:

• put the cursor on a #tensor_view, #float32_view, #ir_view, or #train_log_view command;
• put the cursor on #pytorch_translate_file to preview a PyTorch-to-TorchLean skeleton;
• Lean's infoview renders an interactive panel;
• if you want the full gallery, open NN.Examples.Advanced.Widgets.

This quickstart keeps only the smallest useful examples so the widget path does not feel like a full model zoo.

def NN.Examples.Quickstart.Widgets.vector : Spec.Tensor Float (Tensor.shapeOfDims [4])

A small vector, built with the same typed tensor constructor used in ordinary code.

def NN.Examples.Quickstart.Widgets.matrix : Spec.Tensor ℤ (Tensor.shapeOfDims [2, 3])

A small matrix where the shape is visible both in the type and in the widget.

def NN.Examples.Quickstart.Widgets.one32 : TorchLean.Floats.IEEE754.IEEE32Exec

A binary32 value; the widget shows sign/exponent/fraction fields and classification flags.

def NN.Examples.Quickstart.Widgets.addGraph : IR.Graph

A small IR graph: input plus constant, then an add node.

def NN.Examples.Quickstart.Widgets.tinyTrainLog : Runtime.Training.TrainLog

A minimal train log; real training examples can write the same structure as JSON.

The commands below are ordinary Lean commands that render editor panels through ProofWidgets. They do not alter the definitions above and they are not part of any proof. This is why widgets are safe to keep in quickstarts: deleting the commands leaves the same tensors, graphs, logs, and Python source files behind.

The translator widget is intentionally placed next to the IR/shape widgets. It is a lightweight preview for "what would this PyTorch layer stack look like in TorchLean?" The checked graph-capture path is still the torch.export importer, which parses and validates explicit IR JSON.