🚀 go-pugleaf

Is it possible to write generic predicates in Zed?

For example, consider the definition of concatenation in the
mathematical tool-kit.  First, \cat is defined as a generic
infix.  Then, laws such as:

  \# (s \cat t) = \#s + \#t

are stated.  How do I state the above law in a Zed specification?  If
I try:

\begin{zed}
  \# (s \cat t) = \#s + \#t
\end{zed}

then, fuzz complains about s and t not being declared.  But, if I
declare s and t, then they will have a specific type associated with
them and the law will be about concatenation of that specific type of
sequence rather than generic concatenation??

Todd Fine
fine@sctc.com