Graph layers as NNModuleSpecs #
NN/Spec/Layers/Gnn.lean defines a small GCN-style layer spec:
H' = A · H · W + b
This file wraps that forward spec as an NNModuleSpec so it can be composed in SpecChain
pipelines and carry simple export metadata.
def
Spec.GCNModuleSpec
{α : Type}
[Context α]
{n inDim outDim : ℕ}
(layer : GCNLayerSpec n inDim outDim α)
:
ModSpec.NNModuleSpec α (Shape.dim n (Shape.dim inDim Shape.scalar)) (Shape.dim n (Shape.dim outDim Shape.scalar))
GCN layer wrapper: (n, inDim) -> (n, outDim).