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 values without .cons ... .nil boilerplate.

The sequential macro expands to the composition helpers defined by NN.API.Neural.Builders. The tensor-pack macro expands to constructors under TorchLean.tensorpack.

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

def TorchLean.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 TorchLean.nnSequentialBangLit : Lean.ParserDescr

def TorchLean.tensorpackLit : Lean.ParserDescr

Build a TorchLean.TensorPack from comma-separated tensors.