Eager Tensor Operations

PyTorch-style tensor operations backed by the eager CPU/CUDA tapes. These wrappers record runtime nodes, dispatch CUDA kernels when requested, and preserve the typed TensorRef surface.

Linear algebra and concatenation

def Runtime.Autograd.Torch.Internal.EagerSession.matmul {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {batchA batchB batch : Spec.Shape} {m n p : ℕ} [broadcastA : batchA.BroadcastTo batch] [broadcastB : batchB.BroadcastTo batch] (a : TensorRef α (batchA.concat [m, n])) (b : TensorRef α (batchB.concat [n, p])) : IO (TensorRef α (batch.concat [m, p]))

Matrix multiplication with PyTorch-style broadcasting across batch prefixes.

def Runtime.Autograd.Torch.Internal.EagerSession.concatLeadingAxis {α : Type} [TorchLean.Storage α] (s : EagerSession α) {n m : ℕ} {sh : Spec.Shape} (a : TensorRef α (Spec.Shape.dim n sh)) (b : TensorRef α (Spec.Shape.dim m sh)) : IO (TensorRef α (Spec.Shape.dim (n + m) sh))

Concatenate along dim 0 for tensors with leading dimension. PyTorch: torch.cat(..., dim=0).

def Runtime.Autograd.Torch.Internal.EagerSession.sliceLeadingAxisRange {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Zero α] {n : ℕ} {sh : Spec.Shape} (x : TensorRef α (Spec.Shape.dim n sh)) (start len : ℕ) (h : start + len ≤ n) : IO (TensorRef α (Spec.Shape.dim len sh))

Slice along dim 0: x[start:start+len]. PyTorch: standard slicing.