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, or #train_log_view command;
• Lean's infoview renders an interactive panel;
• graph, rewrite, translator, verification, and RL widgets live in 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 Float [4]

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

def NN.Examples.Quickstart.Widgets.matrix : TorchLean.Tensor ℤ [2, 3]

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

def NN.Examples.Quickstart.Widgets.one32 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) one32._proof_1 one32._proof_2 one32._proof_3 one32._proof_4

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

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. They inspect existing values and do not change runtime behavior or proof status.