Public Tensor Constructors

This module owns the TorchLean.Tensor construction surface: literals, flat-index generation, and bounded-index constructors. The constant constructors full, zeros, and ones live with the specification-layer constructors so that spec code can use them too. Import NN.Tensor for the complete public tensor API.

NN.Spec.Core.FloatInstances supplies FloatLib's configured binary scalar types and their TorchLean contexts, so the same constructors accept both native and configured precisions.

@[instance_reducible]

instance TorchLean.Tensor.scalarOfNat {α : Type} [Storage α] {n : ℕ} [OfNat α n] : OfNat (Tensor α (Shape.ofList [])) n

Lift an integer literal into a rank-zero tensor.

The expected tensor type fixes both the scalar representation and the empty shape, so users can write 1 : Tensor α [] without an explicit constructor.

@[instance_reducible]

instance TorchLean.Tensor.scalarOfScientific {α : Type} [Storage α] [OfScientific α] : OfScientific (Tensor α (Shape.ofList []))

Lift a decimal or scientific literal into a rank-zero tensor.

This is representation-polymorphic: any executable or proof-oriented scalar type with OfScientific receives the same ordinary literal syntax.

def TorchLean.Tensor.oneHot {α : Type} [Storage α] [Zero α] [One α] (n : ℕ) (k : Fin n) : Tensor α [n]

One-hot vector of length n, with a single 1 at index k.

def TorchLean.Tensor.oneHotIndices {α : Type} [Storage α] [Zero α] [One α] (n : ℕ) {s : Shape} : Tensor (Fin n) s → Tensor α (s.appendDim n)

One-hot encode every bounded index along a new final axis.

def TorchLean.Tensor.IndexValidation.indicesInRangeDecidable (n : ℕ) {s : Shape} (x : Tensor ℕ s) : Decidable (Forall (fun (k : ℕ) => k < n) x)

Decide whether every tensor entry is smaller than n.

def TorchLean.Tensor.IndexValidation.boundIndices (n : ℕ) {s : Shape} (x : Tensor ℕ s) : Forall (fun (k : ℕ) => k < n) x → Tensor (Fin n) s

Attach a proved scalar bound to every entry of a tensor.

def TorchLean.Tensor.checkIndices (n : ℕ) {s : Shape} (x : Tensor ℕ s) : Except String (Tensor (Fin n) s)

Validate every natural-number entry and return a tensor of bounded indices.

def TorchLean.Tensor.generateFlat {α : Type} [Storage α] (shape : Shape) (f : ℕ → α) : Tensor α shape

Generate tensor entries from contiguous row-major flat indices.

The buffer is filled directly from the index function; no intermediate array is built.

def TorchLean.Tensor.generateFlatM {m : Type → Type} [Monad m] {α : Type} [Storage α] (shape : Shape) (f : Fin shape.size → m α) : m (Tensor α shape)

Construct a tensor by running one action per row-major coordinate, in increasing flat order.

The result retains the requested shape. A failed action stops construction according to the supplied monad.

def TorchLean.Tensor.stackLeadingM {m : Type → Type} [Monad m] {α : Type} [Storage α] {count : ℕ} {shape : Shape} (components : Fin count → m (Tensor α shape)) : m (Tensor α (shape.prependDim count))

Run one action per leading slice and stack its result, preserving the common trailing shape.

def TorchLean.Tensor.mapM {m : Type → Type} [Monad m] {α β : Type} [Storage α] [Storage β] {shape : Shape} (f : α → m β) (tensor : Tensor α shape) : m (Tensor β shape)

Apply an effectful scalar operation in row-major order, retaining the tensor shape.

def TorchLean.Tensor.scanl {α β : Type} [Storage α] [Storage β] {n : ℕ} (step : β → α → β) (initial : β) (values : Tensor α [n]) : Tensor β [n]

Left-to-right scan with one output per input entry, excluding the initial accumulator.

def TorchLean.Tensor.scanrM {m : Type → Type} [Monad m] {α β : Type} [Storage α] [Storage β] {n : ℕ} (step : α → β → m β) (initial : β) (values : Tensor α [n]) : m (Tensor β [n])

Effectful right-to-left scan, with one output per input entry.

The terminal accumulator is excluded. Effects run from the last input to the first; an error stops the scan according to the supplied monad.

def TorchLean.Tensor.scanr {α β : Type} [Storage α] [Storage β] {n : ℕ} (step : α → β → β) (initial : β) (values : Tensor α [n]) : Tensor β [n]

Right-to-left scan with one output per input entry, excluding the terminal accumulator.

def TorchLean.Tensor.window {α : Type} [Storage α] {count : ℕ} (values : Tensor α [count]) (length : ℕ) (offset : ℕ := 0) (pad : α) : Tensor α [length]

Take a fixed-width tensor window, padding entries past the end.

offset and length determine the result without exposing bounded-index construction. This is the general in-memory constructor used by token, byte, and minibatch window helpers.