@@ -1037,9 +1037,11 @@ automatically:
1037\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
1037\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
1039\medskip\\
1039\medskip\\
1040−\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw)\:\mq\\
1040+\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
1041\hg\hg\edo{
1041\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})
@@ -1051,6 +1053,18 @@ is to be matched.
1051$\MO{MatchWith}$ matches the left hand side of the top level definition against
1053$\MO{MatchWith}$ matches the left hand side of the top level definition against
1052each $\VV{pclause}$, using the result of the match to build each pattern clause
1054each $\VV{pclause}$, using the result of the match to build each pattern clause
1053for $\vx'$.
1055for $\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
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}$.
1056\subsubsection{Elaborating Class and Instance Declarations}
1070\subsubsection{Elaborating Class and Instance Declarations}