Tensor

Tensor inspection widgets for the Lean infoview.

This module defines a #tensor_view t command that displays a small tensor as a rich HTML panel in the infoview. It is designed for:

• examples,
• inspecting runtime output,
• teaching/exposition in the manual.

It is not intended to be used inside proofs, and it is kept out of TorchLean’s default build surface (you must explicitly import NN.Widgets or a concrete widget module such as NN.Widgets.Core.Tensor).

Implementation note: We build on ProofWidgets’ #html command (which ships with mathlib’s dependency set) rather than introducing any custom JavaScript or external build step.

Main definitions

• tensorHtml: shape-aware renderer for typed tensors.
• packedTensorHtml: the same renderer for shape-erased tensors.
• tensorStatsHtml: compact scalar summary (min/max/mean/norms).
• #tensor_view, #anytensor_view, #tensor_stats_view: command entry points.

class NN.Widgets.TensorElemView (α : Type) : Type

Element renderer for #tensor_view.

The tensor widget is used across the library, so we keep element rendering customizable:

• the default instance uses ToString,
• specialized instances can add tooltips (e.g. float32 bits), units, or compact formatting.

• render : α → ProofWidgets.Html

@[instance_reducible]

instance NN.Widgets.instTensorElemViewOfToString {α : Type} [ToString α] : TensorElemView α

Default element renderer for #tensor_view, using ToString.

def NN.Widgets.TensorInternal.prefixEntries {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (tensor : TorchLean.Tensor α s) (limit : ℕ) : Array α

Read only the requested prefix, without converting the full backing buffer.

def NN.Widgets.TensorInternal.renderVector {α : Type} [TorchLean.Storage α] [TensorElemView α] (maxCols : ℕ) {n : ℕ} (t : TorchLean.Tensor α [n]) : ProofWidgets.Html

Render a 1D tensor as a clipped single-row table.

def NN.Widgets.TensorInternal.renderMatrix {α : Type} [TorchLean.Storage α] [TensorElemView α] (maxRows maxCols : ℕ) {n m : ℕ} (t : TorchLean.Tensor α [n, m]) : ProofWidgets.Html

Render a 2D tensor as a clipped grid table.

def NN.Widgets.TensorInternal.renderFlatPreview {α : Type} [TorchLean.Storage α] [ToString α] (maxElems : ℕ) {s : Spec.Shape} (t : TorchLean.Tensor α s) : ProofWidgets.Html

First maxElems entries of a tensor in row-major order, with a marker when there are more.

Truncating matters here: a widget that tried to print a full tensor would hang the editor on anything of realistic size.

def NN.Widgets.tensorHtml {α : Type} [TorchLean.Storage α] [ToString α] [TensorElemView α] {s : Spec.Shape} (t : TorchLean.Tensor α s) (maxRows maxCols : ℕ := 16) (maxElems : ℕ := 64) : ProofWidgets.Html

Render a tensor as HTML.

For small vectors/matrices, we render an actual table; otherwise we show a compact pretty string plus a flat preview.

Runtime Wrappers

def NN.Widgets.packedTensorHtml {α : Type} [TorchLean.Storage α] [ToString α] [TensorElemView α] (v : Spec.SomeTensor α) (maxRows maxCols : ℕ := 16) (maxElems : ℕ := 64) : ProofWidgets.Html

Render a Spec.SomeTensor with the same UI as tensorHtml.

Stats

For small tensors, it is often helpful to inspect numeric ranges without expanding every element. This widget computes simple scalar summaries (min/max/mean/norms).

Main command:

• #tensor_stats_view t

def NN.Widgets.TensorInternal.tensorStatsHtml {α : Type} [TorchLean.Storage α] [Context α] [ToString α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : ProofWidgets.Html

Numeric summary panel: shape, size, extrema, mean, and the three usual norms.

def NN.Widgets.tensorStatsHtml {α : Type} [TorchLean.Storage α] [Context α] [ToString α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : ProofWidgets.Html

Render simple scalar summary statistics (min/max/mean/norms) for a tensor as HTML.

Commands

def NN.Widgets.tensorViewCmd : Lean.ParserDescr

def NN.Widgets.anyTensorViewCmd : Lean.ParserDescr

def NN.Widgets.tensorStatsViewCmd : Lean.ParserDescr

def NN.Widgets.«command#tensor_view_» : Lean.ParserDescr

def NN.Widgets.«command#anytensor_view_» : Lean.ParserDescr

def NN.Widgets.«command#tensor_stats_view_» : Lean.ParserDescr