@@ -1108,9 +1108,50 @@ natToBin' (S (j + j)) odd = True :: natToBin j
11081108\useverb{natToBinwp}
11091109
11101110\noindent
1111−Elaboration of \texttt{with} builds the type declaration and auxiliary function
1112−automatically:
1111+Additionally, the elaborator abstracts over the term being analysed in the type
1112+of the generated auxiliary definition\footnote{This is sometimes referred to
1113+as ``magic \texttt{with}''.} and reorders the arguments as required.
1114+For example:
1115+
1116+\begin{SaveVerbatim}{magicwith}
1117+
1118+f : Nat -> Bool
1119+
1120+ftest : (n : Nat) -> so (f n) -> Nat
1121+ftest n x with (f n)
1122+ | True = ...
1123+ | False = ...
1124+
1125+\end{SaveVerbatim}
1126+\useverb{magicwith}
1127+
1128+\noindent
1129+Here, we may require the knowledge that \texttt{f n} is \texttt{True} or
1130+\texttt{False} in the appropriate case. The elaborator abstracts over
1131+\texttt{f n} in the auxiliary definition, specialising the type of
1132+\texttt{x} in each case:
11131133
1134+\begin{SaveVerbatim}{magicwithaux}
1135+
1136+ftest : (n : Nat) -> so (f n) -> Nat
1137+ftest n x = ftest' n (f n) x
1138+
1139+ftest' : (n : Nat) -> (p : Bool) -> so p -> Nat
1140+ftest' n True x = ...
1141+ftest' n False x = ...
1142+
1143+\end{SaveVerbatim}
1144+\useverb{magicwithaux}
1145+
1146+\noindent
1147+Elaboration of \texttt{with} builds the type declaration and auxiliary function
1148+automatically. It checks the left hand side, resulting in a set of patterns
1149+$\tp$, then splits these patterns into those necessary to type
1150+$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
1151+$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
1152+the matched expression $\ve$ in the types of $\tp_n$.
1153+$\MO{Abstract}\:\ve\:\vw\:\vp$ simply replaces any occurrence of $\vw$ in
1154+$\vp$ with the name $\ve$.
11141155
11151156\DM{
11161157\AR{
@@ -1123,17 +1164,18 @@ automatically:
11231164\MO{NewTerm}\:\TC{Infer};\;
11241165\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
11251166\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1126−\MO{TTDecl}\:(\vx'\Hab\tp\to\vW\to\vT)\\
1127−\tc'\gets\vec{\MO{MatchWith}}\:\tp\:(\vx\:\ttt)\:\vec{\VV{pclause}}\\
1167+(\tp_w,\tp_n)\:\gets\:\MO{SplitContext}\:\vW\:\tp\\
1168+\MO{TTDecl}\:(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\:\ve\:\vw'\:\tp_{n}\to\vT)\\
1169+\tc'\gets\vec{\MO{MatchWith}}\:\tp\:\ttt\:\vec{\VV{pclause}}\\
11281170\vec{\MO{Elab}}\:\tc'\\
1129−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp\:\vw')
1171+\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp_{w}\:\vw'\:\tp_{n})
11301172}
11311173\medskip\\
1132−\MO{MatchWith}\:\tp\:(\vx\:\ttt)\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
1174+\MO{MatchWith}\:\tp_w\:\tp_n\:\ttt\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
11331175\hg\hg\edo{
11341176\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1135−\MO{CheckComplete}\:\tp\:\tp'\\
1136−\RW{return}\:(\vx'\:\tp'\:\ve\:\VV{rhs})
1177+(\tp'_w,\tp'_n)\:\gets\:\MO{SplitPats}\:\tp_w\:\tp_n\:\tp'\\
1178+\RW{return}\:(\vx'\:\tp'_w\:\ve\:\tp'_{n}\:\VV{rhs})
11371179}
11381180}
11391181}
@@ -1154,10 +1196,8 @@ The right hand side, $\VV{rhs}$, may either return a value directly, containing
11541196remains unchanged.
11551197$\MO{Match}\:\vw\:\vt$ returns a list of pattern bindings containing
11561198the variables in $\vt$ and their matches in $\vw$.
1157−If the \texttt{with} block is well-formed, then
1158−the resulting set of patterns $\tp'$ contains exactly the same pattern variables
1159−as $\tp$, which is verified by $\MO{CheckComplete}$.
1160−
1199+The resulting matches are split, using $\MO{SplitPats}$, into matches for those
1200+variables necessary to type $\vW$ and the rest, as before.
11611201
11621202\subsubsection{Elaborating Class and Instance Declarations}
11631203