@@ -1037,9 +1037,11 @@ automatically:
10371037\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
10381038}
10391039\medskip\\
1040−\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw)\:\mq\\
1040+\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
10411041\hg\hg\edo{
1042−
1042+\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1043+\MO{CheckComplete}\:\tp\:\tp'\\
1044+\RW{return}\:(\vx'\:\tp'\:\ve\:\VV{rhs})
10431045}
10441046}
10451047}
@@ -1051,6 +1053,18 @@ is to be matched.
10511053$\MO{MatchWith}$ matches the left hand side of the top level definition against
10521054each $\VV{pclause}$, using the result of the match to build each pattern clause
10531055for $\vx'$.
1056+The clauses in the with block must be of a specific form: they must have an initial
1057+set of arguments $\tw$ which matches the outer clause arguments
1058+$\ttt$, and an extra argument
1059+$\ve$ which is the same type as the scrutinee of the \texttt{with}, $\vW$.
1060+The right hand side, $\VV{rhs}$, may either return a value directly, containing
1061+\texttt{where} clauses, or be a nested \texttt{with} block. In any case, it
1062+remains unchanged.
1063+$\MO{Match}\:\vw\:\vt$ returns a list of pattern bindings containing
1064+the variables in $\vt$ and their matches in $\vw$.
1065+If the \texttt{with} block is well-formed, then
1066+the resulting set of patterns $\tp'$ contains exactly the same pattern variables
1067+as $\tp$, which is verified by $\MO{CheckComplete}$.
10541068
10551069
10561070\subsubsection{Elaborating Class and Instance Declarations}