Quickstart: Widgets

TorchLean widgets are editor-side inspection tools. They render values already present in Lean without changing runtime semantics or proofs.

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.DeepDives.Widgets.

This quickstart keeps only the smallest useful examples; the full widget gallery lives in NN.Examples.DeepDives.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 : Runtime.Training.TrainLog

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

The commands below render editor panels through ProofWidgets. Deleting them leaves the same tensors, graphs, logs, Python source files, and proofs 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.