Tensor

Tensor inspection widgets for the Lean infoview.

Import NN.Widgets or NN.Widgets.Core.Tensor to inspect values through ProofWidgets' #html command. Previews read bounded prefixes and leading slices; the statistics panel scans the whole tensor. Rendering a value does not prove a property of it.

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 default uses ToString; specialized instances can add tooltips, 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.

Vectors and matrices use clipped tables. Higher-rank tensors show bounded leading slices, with a flat preview when the recursion depth is exhausted.

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

#tensor_stats_view t computes extrema, mean, and norms using the scalar's Context operations. Unlike the clipped previews, it materializes and scans every entry.

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 extrema, mean, and norms, scanning every entry with the scalar's arithmetic.

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