I am trying to model mapping a k-ary lambda expression over k row-major matrices, but I cannot seem to get it right. It is really a little more zipWith than map. I have: (extend-reduction-relation ; bla bla... ; bla ... (--> (in-hole S (MAP (λ (x ..._k) e) [[v ..._m] ..._n] ..._k)) (in-hole S [[((λ (x ..._k) e) v ..._k) ..._m] ..._n]))) The idea is to pick the v at the same index pair from each matrix. However, redex complains with syntax: missing ellipsis with pattern variable in template at ..._n. Does redex support this kind of ellipsis shuffling? Or does anyone have an idea what else I could try? :slightly_smiling_face:

A side condition?

In the template (in-hole S [[((λ (x ..._k) e) v ..._k) ..._m] ..._n]), you should not give names to the ellipses. It should be (in-hole S [[((λ (x ...) e) v ...) ...] ...]) instead. As it stands ..._k is a terminal like foo-bar would be a terminal. Then Redex complains about the lack of ellipses when using, for example, the variable x, which was a sequence in the matching pattern.

Hah, thanks. It still doesn’t work, but at least something happens now.