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.

Try these commands 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; the full widget gallery lives in NN.Examples.Advanced.Widgets.

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

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

def NN.Examples.Quickstart.Widgets.matrix : TorchLean.Tensor.T ℤ (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 : TorchLean.Training.TrainLog

A minimal training log; runtime 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 introductory examples: deleting the commands leaves the same tensors, graphs, logs, and Python source files behind.

The translator widget is placed next to the IR/shape widgets. It is a bounded-scope 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.