Elaboration of einsum #
This module implements arbitrary positive-arity einsum over heterogeneous
tensor shapes. Concrete shapes use the executable checker; symbolic shapes
retain their original Nat expressions while proving repeated-label,
broadcasting, source-occurrence, and output-shape invariants.
Elaborate arbitrary positive-arity einsum syntax to the generic verified lowering, reflecting concrete checks or proving symbolic shape invariants.