Small Convenience Macros

This file contains only general-purpose syntactic sugar:

• seq! a, b, c for composing TorchLean Seq models without chaining >>> manually.
• tlist! x, y, ... for building TorchLean.TList 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

For naming-convention friendliness, we also provide the lowercase alias nn.sequential![...]. It expands to the same seeded-builder composition as nn.Sequential![...].

def NN.API.nnSequentialBangLitLower : Lean.ParserDescr

def NN.API.tlistLit : Lean.ParserDescr

Build a TorchLean.TList from comma-separated tensors (avoids .cons ... .nil boilerplate).

This stays compact: it is just a syntactic convenience for examples and small programs.