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.Entrypoint.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.
• anyTensorHtml: same renderer for runtime shape-erased tensors.
• tensorStatsHtml: compact scalar summary (min/max/mean/norms).
• #tensor_view, #anytensor_view, #tensor_stats_view: command entry points.

Implementation notes

• Table rendering for small tensors plus clipped previews for large ones balances readability/performance tradeoff in infoview.
• Element rendering is class-based (TensorElemView) so backends can customize display without forking widget logic.
• We cap recursion depth for higher-rank tensors to avoid overwhelming nested expansions.

References

• ProofWidgets
• Lean community documentation style

Tags

tensor, visualization, stats, proofwidgets, inspection

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

@[implicit_reducible]

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

Default element renderer for #tensor_view, using ToString.

def NN.Widgets.TensorInternal.join (sep : String) (xs : List String) : String

Join strings with a separator.

def NN.Widgets.TensorInternal.dimsString (s : Spec.Shape) : String

Render shape dimensions as a bracketed list string.

def NN.Widgets.TensorInternal.fmtMaybe (x : Option String) : ProofWidgets.Html

def NN.Widgets.TensorInternal.renderVector {α : Type} [TensorElemView α] (maxCols : ℕ) {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : ProofWidgets.Html

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

def NN.Widgets.TensorInternal.renderMatrix {α : Type} [TensorElemView α] (maxRows maxCols : ℕ) {n m : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n (Spec.Shape.dim m Spec.Shape.scalar))) : ProofWidgets.Html

Render a 2D tensor as a clipped grid table.

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

def NN.Widgets.tensorHtml {α : Type} [ToString α] {s : Spec.Shape} (t : Spec.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.anyTensorHtml {α : Type} [ToString α] (v : Runtime.AnyTensor α) (maxRows maxCols : ℕ := 16) (maxElems : ℕ := 64) : ProofWidgets.Html

Render a Runtime.AnyTensor (shape-erased runtime tensor) with the same UI as tensorHtml.

Stats

For small tensors, it is often helpful to quickly sanity-check 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.abs' {α : Type} [Context α] (x : α) : α

def NN.Widgets.TensorInternal.sqrt' {α : Type} [Context α] (x : α) : α

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

def NN.Widgets.tensorStatsHtml {α : Type} [Context α] [ToString α] {s : Spec.Shape} (t : Spec.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