TorchLean Trainer Construction

Public constructors for the unified trainer handle.

class TorchLean.Trainer.ToModel (model : Type u) (σ τ : outParam Shape) : Type (max 2 u)

Values that can be used as public trainer models.

This class lets Trainer.new accept either a seedable model builder or an already-built checked model:

Trainer.new modelBuilder ...
Trainer.new alreadyBuiltModel ...

The seed is consumed only by the builder case. Already-built models pass through unchanged.

• build : ℕ → model → nn.Sequential σ τ

  Materialize the model, using the seed only when the value still needs initialization.

@[implicit_reducible]

instance TorchLean.Trainer.instToModelSequential {σ τ : Shape} : ToModel (nn.Sequential σ τ) σ τ

@[implicit_reducible]

instance TorchLean.Trainer.instToModelMSequential {σ τ : Shape} : ToModel (nn.M (nn.Sequential σ τ)) σ τ

def TorchLean.Trainer.new {model : Type u} {σ τ : Shape} [ToModel model σ τ] (m : model) (cfg : Config σ τ := { }) : Handle σ τ

Build one unified public trainer from a sequential model or seedable model builder.

@[reducible, inline]

abbrev TorchLean.Trainer (σ τ : Shape) : Type 2

Public trainer type carrying a model, task, runtime configuration, and seed.