Quickstart: Tensor Basics

This is the first stop in the TorchLean examples. It does not use sessions, CUDA, or autograd. It is just about building typed tensors in Lean with a convenient constructor layer.

What it covers:

• 1D and N-D constructors from literal lists (Tensor.vector, Tensor.ofList, tensor!),
• the fact that the element type α is the “dtype” (e.g. Float, ℚ, Int),
• Float-literal convenience constructors for executable float32 (Tensor.float32Vector),
• why we generally do not try to print tensors over ℝ (noncomputable / too large).

Run: lake exe torchlean quickstart_tensors

def NN.Examples.Quickstart.TensorBasics.usage : String

Command-line help for the tensor-basics quickstart.

def NN.Examples.Quickstart.TensorBasics.main (args : List String) : IO Unit