TorchLean Public Names

Root public names and training-log types used by import NN.

@[reducible, inline]

abbrev TorchLean.Shape : Type

Tensor shape descriptor used to index spec-level tensors (Spec.Tensor α s).

Shape is an outermost-first tree:

• .scalar for a scalar,
• .dim n s for a length-n dimension whose entries have shape s.

@[reducible, inline]

abbrev TorchLean.Options : Type

Runtime options such as backend, dtype, and CUDA fast-kernel selection.

@[reducible, inline]

abbrev TorchLean.SupervisedSample (α : Type) (σ τ : Spec.Shape) : Type

One supervised training example with an input tensor and target tensor.

@[reducible, inline]

abbrev TorchLean.SequentialModel : Spec.Shape → Spec.Shape → Type 2

Shape-indexed sequential model. Most examples use the shorter nn.Sequential spelling.

@[reducible, inline]

abbrev TorchLean.ModelBuilder (α : Type u_1) : Type u_1

Randomized model builder used by nn.run and built-in examples.

@[reducible, inline]

abbrev TorchLean.modelParamShapes {σ τ : Shape} (model : SequentialModel σ τ) : List Shape

Parameter shapes required by a sequential model.

@[reducible, inline]

abbrev TorchLean.TensorPack (α : Type) (shapes : List Shape) : Type

Shape-indexed tensor pack.

This is the public name for TorchLean's typed tuple/argument-pack representation. A TensorPack α [s₁, s₂, ...] is a fixed tuple of tensors whose shapes are tracked by the type-level list.

@[reducible, inline]

abbrev TorchLean.ParamTensors (α : Type) (shapes : List Shape) : Type

Concrete parameter tensors for a model or model slice.

This is the root public name for shape-indexed parameter tensors. The nn.ParamTensors spelling points back to this same type so model code can stay on the shorter name.

@[reducible, inline]

abbrev TorchLean.ScalarModuleDef (paramShapes inputShapes : List Spec.Shape) : Type 1

Shape-indexed module definition used by the executable TorchLean training runtime.

@[reducible, inline]

abbrev TorchLean.LossReduction : Type

How a vector of per-example losses is reduced to one scalar loss.

@[reducible, inline]

abbrev TorchLean.CsvOptions : Type

CSV parsing options used by the public data loaders.

@[reducible, inline]

abbrev TorchLean.Training.Curve : Type

A scalar metric curve, usually a loss or accuracy series over training steps.

@[reducible, inline]

abbrev TorchLean.Training.TrainLog : Type

JSON-serializable training log with metrics and run metadata.

@[reducible, inline]

abbrev TorchLean.Training.ExperimentLog : Type

Mutable experiment log used by longer-running examples.

@[reducible, inline]

abbrev TorchLean.Training.LogDestination : Type

Output destination for training logs.

@[reducible, inline]

abbrev TorchLean.Training.MetricHistory : Type

In-memory history for named training metrics.

@[reducible, inline]

abbrev TorchLean.Training.Dataset (a : Type) : Type

Finite in-memory dataset used by TorchLean trainers.

@[reducible, inline]

abbrev TorchLean.Training.DataLoader (a : Type) : Type

Stateful minibatch loader for finite datasets.