Small Convenience Macros

This file contains only general-purpose syntactic sugar:

• seq! a, b, c for composing TorchLean Seq models without chaining >>> manually.
• tensorpack! x, y, ... for building TorchLean.tensorpack.TensorPack values without .cons ... .nil boilerplate.

Both macros expand to fully-qualified names under NN.API.TorchLean.*, so in practice you will usually import NN.API.Public (or at least NN.API.Runtime) alongside this module.

We avoid layer-specific "proof-eliding" macros here; prefer the named-field APIs in NN.API.Public for clarity and stable documentation.

def NN.API.seqLit : Lean.ParserDescr

Compose Seq models without chaining >>> manually.

Sequential Literals

TorchLean sequential models are shape-indexed (Seq σ τ), so we cannot use a plain List of layers like PyTorch does (a List would require every element to have the same type).

Instead we provide macros that expand to ordinary Seq composition while still letting users write “list-shaped” model definitions.

def NN.API.nnSequentialBangLit : Lean.ParserDescr

def NN.API.tensorpackLit : Lean.ParserDescr

Build a TorchLean.tensorpack.TensorPack from comma-separated tensors.