@@ -49,18 +49,18 @@ instantiating one such variable also instantiates all of its dependencies.
4949\FFIG{
5050\begin{array}{c}
5151\vb ::= \ldots
52− \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:
53− \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})
52+ \;\mid\; \hole{\vx}{\vt} \;\;(\mbox{hole binding}) \;\;
53+ \;\mid\; \guess{\vx}{\vt}{\vt} \;\;(\mbox{guess})
5454\medskip\\
55−\mathsf{HoleVar}\:
55+\mathsf{HoleVar}\;
5656\Rule{(\hole{\vx}{\vS})\in\Gamma}
5757{\Gamma\vdash\vx\Hab\vS}
5858\hg
59−\mathsf{GuessVar}\:
59+\mathsf{GuessVar}\;
6060\Rule{(\guess{\vx}{\vS}{\vs})\in\Gamma}
6161{\Gamma\vdash\vx\Hab\vS}
6262\\
63−\mathsf{Hole}\:
63+\mathsf{Hole}\;
6464\Rule{
6565\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT
6666}
@@ -69,7 +69,7 @@ instantiating one such variable also instantiates all of its dependencies.
6969}
7070%\hspace*{0.1cm}\vx\not\in\vT
7171\hg
72−\mathsf{Guess}\:
72+\mathsf{Guess}\;
7373\Rule{
7474\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT
7575}
@@ -127,12 +127,12 @@ Exceptions are captured by the option type $\MO{Result}$ which
127127either indicates success, or reports an error $\MO{Err}$:
128128
129129\DM{
130−\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
130+\RW{data}\;\MO{Result}\;\vt\;=\;\MO{Success}\;\vt\;\mid\;\MO{Failure}\;\MO{Err}
131131}
132132
133133\noindent
134134If any operation fails during a proof (e.g. a subterm fails to type check)
135−then the entire proof fails (i.e. returns $\MO{Failure}\:\ve$ with some error
135+then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error
136136message $\ve$) unless otherwise handled.
137137
138138The \texttt{Elab} monad supports various operations for querying and updating
@@ -172,7 +172,7 @@ contain hole or guess bindings, it may nevertheless \remph{refer} to hole- or
172172guess-bound variables.
173173
174174The proof state is initialised with the $\MO{NewProof}$ operation. Given a
175−global context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
175+global context $\vC$, $\MO{NewProof}\;\vt$ sets up the proof state as:
176176
177177\DM{
178178(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)
@@ -181,7 +181,7 @@ global context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:
181181The local context is initially empty, and the initial hole queue is the $\vx$ standing for
182182the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.
183183In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
184−$\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and
184+$\MO{NewTerm}\;\vt$ discards the proof term and hole queue, and
185185updates the proof state to:
186186
187187\DM{
@@ -211,21 +211,21 @@ may fail. We have the following primitive meta-operations:
211211\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
212212% Focus and Unfocus don't need to be primitive, we could show in terms of
213213% Get and Put
214−%\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
214+%\item $\MO{Focus}\;\vn$, which moves $\vn$ to the head of the hole queue.
215215%\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
216−\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
216+\item $\Check\;\ve$, which type checks an expression $\ve$ relative to a context
217217$\Gamma$, returning its type.
218218$\MO{Check}$ will fail
219219if the expression is not well-typed.
220−\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context
220+\item $\Eval\;\ve$, which evaluates a well-typed expression $\ve$ relative to a context
221221$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,
222222but does not reduce definitions which are not total.
223223\item
224−$\PrimUnify\:\ve_1\:\ve_2$,
224+$\PrimUnify\;\ve_1\;\ve_2$,
225225which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
226226holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
227227to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).
228−\item $\Subst\:\vx\:\ve$, which instantiates a hole $\vx$ directly with a term
228+\item $\Subst\;\vx\;\ve$, which instantiates a hole $\vx$ directly with a term
229229$\ve$, typically arising from unification.
230230\end{itemize}
231231
@@ -233,12 +233,12 @@ $\ve$, typically arising from unification.
233233Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
234234and $\MO{NextHole}$
235235operations which manipulate and inspect
236−the hole queue. $\MO{Focus}\:\vn$ moves a hole to the head of the hole queue:
236+the hole queue. $\MO{Focus}\;\vn$ moves a hole to the head of the hole queue:
237237
238238\DM{
239−\MO{Focus}\:\vn\:=\:\RW{do}\:\AR{
239+\MO{Focus}\;\vn\;=\;\RW{do}\;\AR{
240240(\vC,\Delta,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\
241−\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ;\vQ')\\
241+\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ;\vQ')\\
242242}
243243}
244244
@@ -247,9 +247,9 @@ Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the
247247end of the hole queue:
248248
249249\DM{
250−\MO{Unfocus}\:=\:\RW{do}\:\AR{
250+\MO{Unfocus}\;=\;\RW{do}\;\AR{
251251(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
252−\MO{Put}\:(\vC,\Delta,\vP,\vQ;\vn)\\
252+\MO{Put}\;(\vC,\Delta,\vP,\vQ;\vn)\\
253253}
254254}
255255
@@ -259,14 +259,14 @@ next, and $\MO{NextHole}$ returns the next hole to be solved:
259259
260260\DM{
261261\AR{
262−\MO{NewHole}\:=\:\RW{do}\:\AR{
262+\MO{NewHole}\;=\;\RW{do}\;\AR{
263263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
264−\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
264+\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ)\\
265265}
266266\\
267−\MO{NextHole}\:=\:\RW{do}\:\AR{
267+\MO{NextHole}\;=\;\RW{do}\;\AR{
268268(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
269−\MO{Return}\:\vn
269+\MO{Return}\;\vn
270270}
271271}
272272}
@@ -278,7 +278,7 @@ form:
278278
279279\DM{
280280\PA{\A\A}{
281−\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
281+\MO{Tactic}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\vt'}
282282}
283283}
284284
@@ -304,40 +304,40 @@ tactic.
304304
305305\FFIG{
306306\AR{
307−\MO{Tactic}\:\VV{tac}\:=\:\RW{do}\:\AR{
307+\MO{Tactic}\;\VV{tac}\;=\;\RW{do}\;\AR{
308308\ve\Gets\MO{Term}\\
309309\vh\Gets\MO{NextHole}\\
310−\ve'\Gets\MO{Tactic'}\:\langle\rangle\:\ve\:\VV{tac}\:\vh\\
311−\MO{SetTerm}\:\ve'
310+\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\;\VV{tac}\;\vh\\
311+\MO{SetTerm}\;\ve'
312312}
313313\medskip
314314\\
315315\PA{\A\A\A}{
316316\RW{where} \\
317317& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)
318−& \MoRet{\VV{tac}_\Gamma\:(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\:\vx=\vh} \\
318+& \MoRet{\VV{tac}_\Gamma\;(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\
319319& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)
320−& \MoRet{\VV{tac}_\Gamma\:(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\:\vx=\vh} \\
320+& \MoRet{\VV{tac}_\Gamma\;(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\
321321& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
322322& \MoRet{
323−\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
324−\lam{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\lam{\vx}{\vT'})\:\ve}
323+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
324+\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve}
325325}
326326\\
327327& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
328328& \MoRet{
329−\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
330−\all{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\all{\vx}{\vT'})\:\ve}
329+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
330+\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve}
331331}
332332\\
333−& \MO{Tactic'} & \Gamma & (\LET\:\vx\defq\vt\Hab\vT\SC\ve)
334−& \MoRet{\RW{do}\:\AR{\vt'\Gets\:\MO{Tactic'}\:\Gamma\:\vt\\
335−\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
336−\LET\:\vx\defq\vt'\Hab\vT'\SC
337−\MO{Tactic'}\:(\Gamma;\LET\:\vx\defq\vt'\Hab\vT')\:\ve}} \\
338−& \MO{Tactic'} & \Gamma & (\vf\:\va) &
339−\MoRet{\MO{Return}\:(\MO{Tactic'}\:\Gamma\:\vf)\: (\MO{Tactic'}\:\Gamma\:\va)}\\
340−& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\:\vt}
333+& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)
334+& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\
335+\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
336+\LET\;\vx\defq\vt'\Hab\vT'\SC
337+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve}} \\
338+& \MO{Tactic'} & \Gamma & (\vf\;\va) &
339+\MoRet{\MO{Return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\
340+& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\;\vt}
341341}
342342}
343343}
@@ -359,10 +359,10 @@ affect the solution to other unification problems. Instead,
359359$\MO{PrimUnify}$ may give one of the following results:
360360
361361\begin{itemize}
362−\item $\MO{Success}\:(\tx=\te, \tp)$, containing the solved holes mapping
362+\item $\MO{Success}\;(\tx=\te, \tp)$, containing the solved holes mapping
363363$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
364364If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
365−\item $\MO{Failure}\:\ve$, if no solution is found due to a failure to unify
365+\item $\MO{Failure}\;\ve$, if no solution is found due to a failure to unify
366366sub-terms in normal form.
367367\end{itemize}
368368
@@ -381,21 +381,21 @@ resolve the existing problems with $\MO{ReUnify}$.
381381%operation to update
382382%the proof state with new problems, and solve the old ones
383383\AR{
384−\Unify\:\ve_1\:\ve_2\:=\:\RW{do}\:
384+\Unify\;\ve_1\;\ve_2\;=\;\RW{do}\;
385385\AR{
386−(\tx=\te,\tp)\gets\PrimUnify\:\ve_1\:\ve_2\\
387−\vec{\MO{Subst}}\:\tx\:\te\\
388−\MO{SubstProblems}\:(\tx=\te)\\
386+(\tx=\te,\tp)\gets\PrimUnify\;\ve_1\;\ve_2\\
387+\vec{\MO{Subst}}\;\tx\;\te\\
388+\MO{SubstProblems}\;(\tx=\te)\\
389389(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\
390−\vec{\MO{ReUnify}}\:\tP
390+\vec{\MO{ReUnify}}\;\tP
391391}
392392\medskip
393393\\
394394\AR{
395−\MO{ReUnify}\:(\Gamma,\ve_1,\ve_2)\:=\:\RW{do}\:\AR{
396−(\tx=\te,\tp)\Gets\PrimUnify\:\ve_1\:\ve_2\\
397−\vec{\MO{Subst}}\:\tx\:\te\\
398−\MO{Return}\:\tp
395+\MO{ReUnify}\;(\Gamma,\ve_1,\ve_2)\;=\;\RW{do}\;\AR{
396+(\tx=\te,\tp)\Gets\PrimUnify\;\ve_1\;\ve_2\\
397+\vec{\MO{Subst}}\;\tx\;\te\\
398+\MO{Return}\;\tp
399399}
400400}
401401}
@@ -413,7 +413,7 @@ keeping $\vx$ at the head:
413413\DM{
414414\PA{\A\A}{
415415\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
416− \MoRet{\RW{return}\:\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
416+ \MoRet{\RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
417417}
418418}
419419
@@ -429,10 +429,10 @@ solve other holes by unifying the expected type of $\vx$ with the type of $\vv$:
429429\DM{
430430\PA{\A\A}{
431431\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
432− \MoRet{\RW{do}\:\AR{
433− \vT' \leftarrow \Check\:\vv\\
434− \Unify\:\vT\:\vT'\\
435− \RW{return}\:\guess{\vx}{\vT}{\vv}\SC\ve}
432+ \MoRet{\RW{do}\;\AR{
433+ \vT' \leftarrow \Check\;\vv\\
434+ \Unify\;\vT\;\vT'\\
435+ \RW{return}\;\guess{\vx}{\vT}{\vv}\SC\ve}
436436 } \\
437437}
438438}
@@ -443,9 +443,9 @@ For example, consider the following proof term:
443443\DM{
444444\AR{
445445\hole{\vA}{\Type}\SC\hole{\vk}{\Nat}\SC
446−\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\:\vA\:\vk}\SC
446+\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\;\vA\;\vk}\SC
447447\\
448−\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys
448+\hole{\vys}{\Vect\;\vA\;(\suc\;\vk)}\SC\vys
449449}
450450}
451451
@@ -455,9 +455,9 @@ attempts to
455455$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:
456456
457457\begin{itemize}
458−\item $\Check\:42\:\mq\:\TC{Int}$
458+\item $\Check\;42\;\mq\;\TC{Int}$
459459\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if
460−$\vA\:=\:\TC{Int}$, so solve $\vA$.
460+$\vA\;=\;\TC{Int}$, so solve $\vA$.
461461\end{itemize}
462462
463463\noindent
@@ -466,9 +466,9 @@ Therefore the resulting proof term is:
466466\DM{
467467\AR{
468468\hole{\vk}{\Nat}\SC
469−\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\:\TC{Int}\:\vk}\SC
469+\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\;\TC{Int}\;\vk}\SC
470470\\
471−\hole{\vys}{\Vect\:\TC{Int}\:(\suc\:\vk)}\SC\vys
471+\hole{\vys}{\Vect\;\TC{Int}\;(\suc\;\vk)}\SC\vys
472472}
473473}
474474
@@ -479,7 +479,7 @@ the guess is substituted into its scope:
479479\DM{
480480\PA{\A}{
481481\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
482− \MoRet{\RW{return}\:\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\:\vv$)}}
482+ \MoRet{\RW{return}\;\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\;\vv$)}}
483483}
484484}
485485
@@ -495,9 +495,9 @@ handle failure using the $\MO{Try}$ tactic combinator:
495495\DM{
496496\PA{\A\A\A}{
497497\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
498− \MoRet{\RW{case}\:\AR{\VV{t1}_\Gamma\:\vt\:\RW{of}\\
499− \MO{Success}\:\vt'\cq\MO{Success}\:\vt'\\
500− \MO{Failure}\:\_\cq\VV{t2}_\Gamma\:\vt\\
498+ \MoRet{\RW{case}\;\AR{\VV{t1}_\Gamma\;\vt\;\RW{of}\\
499+ \MO{Success}\;\vt'\cq\MO{Success}\;\vt'\\
500+ \MO{Failure}\;\_\cq\VV{t2}_\Gamma\;\vt\\
501501 }}
502502}
503503}
@@ -514,9 +514,9 @@ binding requires that the goal normalises to a function type:
514514\DM{
515515\PA{\A\A}{
516516\MO{Lambda}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\vx) &
517− \MoRet{\RW{do}\:\AR{
518− \all{\vy}{\vS}\SC\vT'\:\leftarrow\:\Eval\:\vT \\
519− \RW{return}\:\lam{\vn}{\vS}\SC\hole{\vx}{\vT'[\vn/\vy]}\SC\vx
517+ \MoRet{\RW{do}\;\AR{
518+ \all{\vy}{\vS}\SC\vT'\;\leftarrow\;\Eval\;\vT \\
519+ \RW{return}\;\lam{\vn}{\vS}\SC\hole{\vx}{\vT'[\vn/\vy]}\SC\vx
520520 }
521521 }
522522}
@@ -528,9 +528,9 @@ Creating a $\forall$ binding requires that the goal is a $\TC{Type}$:
528528\DM{
529529\PA{\A\A}{
530530\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &
531− \MoRet{\RW{do}\:\AR{
532− \Type\:\leftarrow\:\Check\:\vS\\
533− \RW{return}\:\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx
531+ \MoRet{\RW{do}\;\AR{
532+ \Type\;\leftarrow\;\Check\;\vS\\
533+ \RW{return}\;\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx
534534 }
535535 }
536536}
@@ -542,11 +542,11 @@ Creating a $\LET$ binding requires a type and a value.
542542\DM{
543543\PA{\A\A}{
544544\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &
545− \MoRet{\RW{do}\:\AR{
546− \Type\:\leftarrow\:\Check\:\vS\\
547− \vS'\:\leftarrow\:\Check\:\vv\\
548− \Unify\:\vS\:\vS'\\
549− \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
545+ \MoRet{\RW{do}\;\AR{
546+ \Type\;\leftarrow\;\Check\;\vS\\
547+ \vS'\;\leftarrow\;\Check\;\vv\\
548+ \Unify\;\vS\;\vS'\\
549+ \RW{return}\;\LET\;\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
550550 }
551551 }
552552}
@@ -563,7 +563,7 @@ head of the queue:
563563\DM{
564564\PA{\A}{
565565\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
566− \MoRet{\RW{do}\:\AR{
566+ \MoRet{\RW{do}\;\AR{
567567 \MO{NewHole}\;\vx'\\
568568 \RW{return}\;\guess{\vx}{\vT}{(\hole{\vx'}{\vT}\SC\vx')}\SC\ve}}
569569}
@@ -573,17 +573,17 @@ head of the queue:
573573For example, consider the following proof term:
574574
575575\DM{
576−\hole{\vx}{\va\to\vb}\SC\vx\:\ve
576+\hole{\vx}{\va\to\vb}\SC\vx\;\ve
577577}
578578
579579\noindent
580580If we try to instantiate $\vx$ with a $\lambda$-binding $\vn$ immediately,
581581without applying $\MO{Attack}$ first, the $\lambda$ will scope over the
582−entirety of $\vx\:\ve$, and the resulting term is not well-typed:
582+entirety of $\vx\;\ve$, and the resulting term is not well-typed:
583583
584584\DM{
585585\AR{
586−\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\:\ve
586+\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\;\ve
587587}
588588}
589589
@@ -593,10 +593,10 @@ a $\lambda$ binding $\vn$, we get:
593593
594594\DM{
595595\begin{array}{ll}
596−\guess{\vx}{\va\to\vb}{\hole{\vx'}{\va\to\vb}\SC\vx'}\SC\vx\:\ve
596+\guess{\vx}{\va\to\vb}{\hole{\vx'}{\va\to\vb}\SC\vx'}\SC\vx\;\ve
597597& \hg\mbox{(after $\MO{Attack}$)}\\
598−\guess{\vx}{\va\to\vb}{\lam{\vn}{\va}\SC\hole{\vx'}{\vb}\SC\vx'}\SC\vx\:\ve
599−& \hg\mbox{(after $\MO{Lambda}\:\vn$)}
598+\guess{\vx}{\va\to\vb}{\lam{\vn}{\va}\SC\hole{\vx'}{\vb}\SC\vx'}\SC\vx\;\ve
599+& \hg\mbox{(after $\MO{Lambda}\;\vn$)}
600600\end{array}
601601}
602602
@@ -614,9 +614,9 @@ with the pattern variable directly:
614614\DM{
615615\PA{\A\A}{
616616\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &
617− \MoRet{\RW{do}\:\AR{
618− \MO{PatBind}\:(\vn\Hab\vT)\\
619− \RW{return}\:\ve[\vn/\vx]
617+ \MoRet{\RW{do}\;\AR{
618+ \MO{PatBind}\;(\vn\Hab\vT)\\
619+ \RW{return}\;\ve[\vn/\vx]
620620 }}
621621}
622622}
@@ -635,7 +635,7 @@ complete term by refining a proof state, let us consider the following
635635\DM{
636636\AR{
637637\FN{id}\Hab\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
638−\FN{id}\:=\:\lam{\vA}{\Type}\SC\lam{\va}{\vA}\SC\va
638+\FN{id}\;=\;\lam{\vA}{\Type}\SC\lam{\va}{\vA}\SC\va
639639}
640640}
641641
@@ -647,9 +647,9 @@ the goal type.
647647
648648\DM{
649649\AR{
650−\MO{MkId}\:\mq\:\RW{do}\:
650+\MO{MkId}\;\mq\;\RW{do}\;
651651 \AR{
652− \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
652+ \MO{NewProof}\;\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
653653 \MO{Tactic}\;\MO{Attack} \\
654654 \MO{Tactic}\;(\MO{Lambda}\;\vA) \\
655655 \MO{Tactic}\;\MO{Attack} \\
@@ -683,7 +683,7 @@ the goal type.
683683&
684684\langle\vh_0,\vx\rangle\\
685685%
686−\MO{Lambda}\:\vA &
686+\MO{Lambda}\;\vA &
687687\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
688688\underline{
689689\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
@@ -706,7 +706,7 @@ the goal type.
706706&
707707\langle\vh_1,\vh_0,\vx\rangle\\
708708%
709−\MO{Lambda}\:\va &
709+\MO{Lambda}\;\va &
710710\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
711711\lam{\vA}{\Type}\SC
712712\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
@@ -721,7 +721,7 @@ the goal type.
721721&
722722\langle\vh_1,\vh_0,\vx\rangle\\
723723%
724−\MO{Fill}\:\va &
724+\MO{Fill}\;\va &
725725\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
726726\lam{\vA}{\Type}\SC
727727\\
@@ -807,19 +807,19 @@ a Coq proof script.
807807
808808\FFIG{
809809\AR{
810−\MO{MkIdType}\:\mq\:\RW{do}\;
810+\MO{MkIdType}\;\mq\;\RW{do}\;
811811 \AR{
812− \MO{NewProof}\:\Type\\
813− \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Type) ;
814− \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\
812+ \MO{NewProof}\;\Type\\
813+ \MO{Attack} ; \MO{Pi}\;(\vA\Hab\Type) ;
814+ \MO{Attack} ; \MO{Pi}\;(\va\Hab\vA) \\
815815 \MO{Fill}\;\vA \\
816816 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\
817817 \MO{Term}
818818 }
819819 \medskip\\
820−\MO{MkId}\:\mq\:\RW{do}\;
820+\MO{MkId}\;\mq\;\RW{do}\;
821821 \AR{
822− \vt\:\leftarrow\:\MO{MkIdType}; \MO{NewProof}\:\vt\\
822+ \vt\;\leftarrow\;\MO{MkIdType}; \MO{NewProof}\;\vt\\
823823 \MO{Attack} ; \MO{Lambda}\;\vA ;
824824 \MO{Attack} ; \MO{Lambda}\;\va \\
825825 \MO{Fill}\;\va \\
@@ -928,11 +928,11 @@ are given explicitly, the application must be expanded.
928928\begin{array}{rll@{\hg}rll}
929929\ve ::= & \vc & (\mbox{constant}) &
930930\mid & \vx & (\mbox{variable}) \\
931−\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
932−\mid & \ve\:\ta & (\mbox{function application}) \\
933−\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) &
931+\mid & \ilam{\vx}\;\ve & (\mbox{lambda abstraction}) &
932+\mid & \ve\;\ta & (\mbox{function application}) \\
933+\mid & \ilet{\vx}{\ve}\;\ve & (\mbox{let binding}) &
934934\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
935−%\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
935+%\mid & \icase\;\ve\;\iof\;\vec{\VV{alt}} & (\mbox{case expression}) &
936936%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
937937\mid & \_ & (\mbox{placeholder})
938938\end{array}
@@ -971,9 +971,9 @@ are given explicitly, the application must be expanded.
971971\begin{array}{ll}
972972\begin{array}{rll}
973973\VV{pclause} ::= &
974−\vx\:\ttt\:[\ibar\;\te]\mbox{\texttt{ = }}\ve \hg[\iwhere\;\td]\\
974+\vx\;\ttt\;[\ibar\;\te]\mbox{\texttt{ = }}\ve \hg[\iwhere\;\td]\\
975975\mid & \AR{
976−\vx\:\ttt\:[\ibar\;\te]\;\iwith\;\ve\\
976+\vx\;\ttt\;[\ibar\;\te]\;\iwith\;\ve\\
977977\hg\vec{\VV{pclause}}
978978}
979979\end{array}
@@ -984,7 +984,7 @@ are given explicitly, the application must be expanded.
984984\medskip\\
985985\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td
986986\\
987−\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td
987+\VV{idecl} ::= & \iinstance\;[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td
988988\end{array}
989989\end{array}
990990}
@@ -997,8 +997,8 @@ and declaration syntax given in Figure \ref{idrismd}.
997997\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
998998tuple syntax, \texttt{do}-notation or infix operators --- and with implicit
999999arguments in types bound explicitly
1000−(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\:\va\:\vn$
1001−instead of simply $\Vect\:\va\:\vn$).
1000+(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$
1001+instead of simply $\Vect\;\va\;\vn$).
10021002Note that we separate implicit and type constraint bindings, to ensure that they
10031003only appear in top level declarations.
10041004It is in general straightforward to
@@ -1032,7 +1032,7 @@ has already been set up, which means that elaboration can always be
10321032are building.
10331033
10341034In all cases except the elaboration of variables and constantes,
1035−$\ttpinterp{\vx}\:=\:\ttinterp{\vx}$.
1035+$\ttpinterp{\vx}\;=\;\ttinterp{\vx}$.
10361036
10371037\subsubsection{Elaborating variables and constants}
10381038
@@ -1042,8 +1042,8 @@ the \MO{Fill} tactic:
10421042
10431043\DM{
10441044\AR{
1045−\ttinterp{\vx}\:\mq\:\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve}\\
1046−\ttinterp{\vc}\:\mq\:\RW{do}\:\MO{Fill}\:\vc;\:\MO{Solve}\\
1045+\ttinterp{\vx}\;\mq\;\RW{do}\;\MO{Fill}\;\vx;\;\MO{Solve}\\
1046+\ttinterp{\vc}\;\mq\;\RW{do}\;\MO{Fill}\;\vc;\;\MO{Solve}\\
10471047}
10481048}
10491049
@@ -1059,9 +1059,9 @@ context, we assume that attempting to elaborate a variable which does not type
10591059check means that the variable is a pattern variable:
10601060
10611061\DM{
1062−\ttpinterp{\vx}\:\mq\:
1063−\MO{Try}\:\AR{(\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve})\\
1064−(\MO{Pat}\:\vx)
1062+\ttpinterp{\vx}\;\mq\;
1063+\MO{Try}\;\AR{(\RW{do}\;\MO{Fill}\;\vx;\;\MO{Solve})\\
1064+(\MO{Pat}\;\vx)
10651065}
10661066}
10671067
@@ -1070,13 +1070,14 @@ solve by unification. In this case, we simply move on to the next hole in the qu
10701070the current hole to the end of the queue with $\MO{Unfocus}$:
10711071
10721072\DM{
1073−\ttinterp{\_}\:\mq\:\MO{Unfocus}
1073+\ttinterp{\_}\;\mq\;\MO{Unfocus}
10741074}
10751075
1076−On encountering a placeholder, our assumption is that unification will eventually solve
1077−the hole. At the end of elaboration, any holes remaining unsolved on the left hand side
1078−become pattern variables. If there are any unsolved on the right hand side, elaboration
1079−fails.
1076+On encountering a placeholder, our assumption is that unification will
1077+eventually solve the hole. At the end of elaboration, any holes remaining
1078+unsolved on the left hand side become pattern variables. If there are any
1079+unsolved on the right hand side, elaboration is incomplete and an error will
1080+be reported when the resulting term is type checked.
10801081
10811082\subsubsection{Elaborating bindings}
10821083
@@ -1085,10 +1086,10 @@ $\MO{Lambda}$ tactic, which will fail if the goal is not a function type. We
10851086then elaborate the scope and $\MO{Solve}$, which discharges the $\MO{Attack}$:
10861087
10871088\DM{
1088−\ttinterp{\ilam{\vx}\ve}\:\mq\:
1089−\RW{do}\:
1089+\ttinterp{\ilam{\vx}\ve}\;\mq\;
1090+\RW{do}\;
10901091\AR{
1091−\MO{Attack};\;\MO{Lambda}\:\vx\\
1092+\MO{Attack};\;\MO{Lambda}\;\vx\\
10921093\ttinterp{\ve}\\
10931094\MO{Solve}
10941095}
@@ -1108,12 +1109,12 @@ scope of the binding.
11081109
11091110\DM{
11101111\AR{
1111−\ttinterp{\piexp{\vx}{\vt}\ve}\:\mq\:
1112−\RW{do}\:
1112+\ttinterp{\piexp{\vx}{\vt}\ve}\;\mq\;
1113+\RW{do}\;
11131114\AR{
1114−\MO{Attack};\;\MO{Claim}\:(\vX\Hab\Type)\\
1115−\MO{Pi}\:(\vx\Hab\vX)\\
1116−\MO{Focus}\:\vX\\
1115+\MO{Attack};\;\MO{Claim}\;(\vX\Hab\Type)\\
1116+\MO{Pi}\;(\vx\Hab\vX)\\
1117+\MO{Focus}\;\vX\\
11171118\ttinterp{\vt};\;
11181119\ttinterp{\ve}\\
11191120\MO{Solve}
@@ -1134,13 +1135,13 @@ if elaborating the scope is successful, unification will solve the claimed varia
11341135$\vV$ and $\vX$.
11351136
11361137\DM{
1137−\ttinterp{\ilet{\vx}{\vv}\:{\ve}}\:\mq\:\RW{do}\:
1138+\ttinterp{\ilet{\vx}{\vv}\;{\ve}}\;\mq\;\RW{do}\;
11381139\AR{
11391140\MO{Attack};\;
1140−\MO{Claim}\:(\vX\Hab\Type);\;
1141−\MO{Claim}\:(\vV\Hab\vX)\\
1142−\MO{Let}\:(\vx\Hab\vX\defq\vV)\\
1143−\MO{Focus}\:\vV\\
1141+\MO{Claim}\;(\vX\Hab\Type);\;
1142+\MO{Claim}\;(\vV\Hab\vX)\\
1143+\MO{Let}\;(\vx\Hab\vX\defq\vV)\\
1144+\MO{Focus}\;\vV\\
11441145\ttinterp{\vv};\;
11451146\ttinterp{\ve}
11461147}
@@ -1158,7 +1159,7 @@ In the first case, the elaborator must expand the application to include implici
11581159For example \texttt{vAdd xs ys} is expanded to
11591160\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments
11601161\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation
1161−$\MO{Expand}\:\vx\:\ta$, given a global function name $\vx$ and the
1162+$\MO{Expand}\;\vx\;\ta$, given a global function name $\vx$ and the
11621163arguments supplied by the programmer $\ta$, returns a new argument list
11631164$\ta'$ with implicit and type class arguments added. Each value in
11641165$\ta'$ is paired with an explicit name for the argument.
@@ -1172,17 +1173,17 @@ forms:
11721173
11731174\DM{
11741175\AR{
1175−\MO{Unify}_\Gamma\;\vf\:\TC{Int}\\
1176−\MO{Unify}_\Gamma\;(\vf\:\vx)\:\TC{Int}\\
1177−\MO{Unify}_\Gamma\;(\vf\:\vx)\:(\vg\:\vx)\\
1176+\MO{Unify}_\Gamma\;\vf\;\TC{Int}\\
1177+\MO{Unify}_\Gamma\;(\vf\;\vx)\;\TC{Int}\\
1178+\MO{Unify}_\Gamma\;(\vf\;\vx)\;(\vg\;\vx)\\
11781179}
11791180}
11801181
11811182The first problem has a solution: $\vf=\TC{Int}$. The second and third problems
11821183have no solution without further information. In the second case, we cannot
11831184conclude anything about $\vf$ or $\vx$ just from knowing that
1184−$\vf\:\vx\:=\:\TC{Int}$. In the third case, although we have $\vx\:=\:\vx$ in
1185−argument position, we cannot conclude that $\vf\:=\:\vg$ in general as a
1185+$\vf\;\vx\;=\;\TC{Int}$. In the third case, although we have $\vx\;=\;\vx$ in
1186+argument position, we cannot conclude that $\vf\;=\;\vg$ in general as a
11861187result.
11871188
11881189Once $\vf$ or $\vg$ is solved in some other way, perhaps by being given
@@ -1198,16 +1199,16 @@ Finally, any type class instance arguments are resolved with the
11981199built-in $\MO{Instance}$ tactic.
11991200
12001201\DM{
1201−\ttinterp{\vx\:\ta}\:\mq\:
1202+\ttinterp{\vx\;\ta}\;\mq\;
12021203\AR{
1203−\RW{do}\:
1204+\RW{do}\;
12041205\AR{
1205−(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
1206−\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
1207−\MO{Fill}\:\vx\:\tn\\
1208−\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
1206+(\tn,\tv)\;\gets\;\MO{Expand}\;\vx\;\ta\\
1207+\vec{\MO{Claim}}\;(\tn\Hab\tT)\\
1208+\MO{Fill}\;\vx\;\tn\\
1209+\vec{\MO{Focus}}\;\tn;\;\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
12091210\MO{Solve} \\
1210−\vec{\MO{Instance}}\:\tn\hg\mbox{(for type class constraint argument $\vn$)}
1211+\vec{\MO{Instance}}\;\tn\hg\mbox{(for type class constraint argument $\vn$)}
12111212}
12121213}
12131214}
@@ -1224,12 +1225,12 @@ applied. Since elaboration is type directed, however, there must be an
12241225appropriate type for the function.
12251226
12261227\DM{
1227−\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
1228+\ttinterp{\ve\;\va}\;\mq\;\RW{do}\;
12281229\AR{
1229−\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\
1230−\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\
1231−\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
1232−\MO{Focus}\:\vs;\;\ttinterp{\va}\\
1230+\MO{Claim}\;(\vA\Hab\Type);\;\MO{Claim}\;(\vB\Hab\Type)\\
1231+\MO{Claim}\;(\vf\Hab\vA\to\vB);\;\MO{Claim}\;(\vs\Hab\vA)\\
1232+\MO{Focus}\;\vf;\;\ttinterp{\ve}\\
1233+\MO{Focus}\;\vs;\;\ttinterp{\va}\\
12331234}
12341235}
12351236
@@ -1244,7 +1245,7 @@ relative to the system state (see Section \ref{sect:sysstate}) and has access to
12441245current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate
12451246\IdrisM{} type, function and class declarations into \TT{} declarations.
12461247
1247−\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
1248+\newcommand{\edo}[1]{\RW{do}\;\AR{#1}}
12481249
12491250\subsubsection{Elaborating Type Declarations}
12501251
@@ -1253,11 +1254,11 @@ translating the \IdrisM{} type to a \TT{} type, then adding the resulting type
12531254as a \TT{} declaration:
12541255
12551256\DM{
1256−\MO{Elab}\:(\vx\Hab\vt)\:\mq
1257−\:\edo{\MO{NewProof}\:\Type\\
1257+\MO{Elab}\;(\vx\Hab\vt)\;\mq
1258+\;\edo{\MO{NewProof}\;\Type\\
12581259 \ttinterp{\vt}\\
12591260 \vt'\gets\MO{Term}\\
1260− \MO{TTDecl}\:(\vx\Hab\vt')
1261+ \MO{TTDecl}\;(\vx\Hab\vt')
12611262}}
12621263
12631264The final $\MO{TTDecl}$ takes the result of elaboration, type checks it,
@@ -1274,20 +1275,20 @@ adds a \TT{} data declaration.
12741275
12751276\DM{
12761277\AR{
1277−\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
1278−\hg\hg\mq\:\edo{\MO{NewProof}\:\Type\\
1278+\MO{Elab}\;(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
1279+\hg\hg\mq\;\edo{\MO{NewProof}\;\Type\\
12791280 \ttinterp{\vt}\\
12801281 \vt'\gets\MO{Term}\\
1281− \MO{TTDecl}\:(\vx\Hab\vt')\\
1282− \tc'\gets\vec{\MO{ElabCon}}\:\tc\\
1283− \MO{TTDecl}\:(\Data\:\vx\Hab\vt'\:\Where\:\tc')
1282+ \MO{TTDecl}\;(\vx\Hab\vt')\\
1283+ \tc'\gets\vec{\MO{ElabCon}}\;\tc\\
1284+ \MO{TTDecl}\;(\Data\;\vx\Hab\vt'\;\Where\;\tc')
12841285}
12851286\AR{
1286−\MO{ElabCon}\:(\vx\Hab\vt)\\
1287−\hg\hg\mq\: \edo{\MO{NewProof}\:\Type\\
1287+\MO{ElabCon}\;(\vx\Hab\vt)\\
1288+\hg\hg\mq\; \edo{\MO{NewProof}\;\Type\\
12881289 \ttinterp{\vt}\\
12891290 \vt'\gets\MO{Term}\\
1290− \RW{return}\:(\vx\Hab\vt')
1291+ \RW{return}\;(\vx\Hab\vt')
12911292}
12921293}}}
12931294
@@ -1300,7 +1301,7 @@ to the global context, such as definitions in $\iwhere$ clauses.
13001301First, let us consider the simplest case, with no $\iwhere$ clause:
13011302
13021303\DM{
1303−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
1304+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;?
13041305}
13051306
13061307How does the left hand side get elaborated, given that elaboration is type directed, and
@@ -1312,21 +1313,21 @@ a type $\TC{Infer}$:
13121313\Data\hg\TC{Infer}\Hab\Type\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Type}\SC\va\to\TC{Infer}
13131314}
13141315
1315−Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and
1316+Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\;\_\;(\vx\;\ttt)$ and
13161317extracting the value and unified type when complete.
13171318
13181319\DM{
13191320\AR{
1320−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
1321+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;\\
13211322\hg\hg\edo{
1322−\MO{NewProof}\:\TC{Infer};\;
1323−\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1324−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1323+\MO{NewProof}\;\TC{Infer};\;
1324+\ttpinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1325+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
13251326\tp\gets\MO{Patterns}\\
1326−\MO{NewTerm}\:\vT;\;
1327+\MO{NewTerm}\;\vT;\;
13271328\ttinterp{\ve}\\
13281329\VV{rhs}\gets\MO{Term}\\
1329−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
1330+\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\VV{rhs})
13301331}
13311332}
13321333}
@@ -1340,10 +1341,10 @@ the clauses and adding the resulting collection to \TT{}.
13401341
13411342\DM{
13421343\AR{
1343−\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
1344+\MO{Elab}\;\vec{\VV{pclause}}\;\mq\;
13441345\edo{
1345−\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
1346−\vec{\MO{TTDecl}}\:\tc
1346+\tc\gets\vec{\MO{ElabClause}}\;\vec{\VV{pclause}}\\
1347+\vec{\MO{TTDecl}}\;\tc
13471348}
13481349}
13491350}
@@ -1355,18 +1356,18 @@ which are then recursively elaborated before the right hand side.
13551356
13561357\DM{
13571358\AR{
1358−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
1359+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve\;\iwhere\;\td)\;\mq\;\\
13591360\hg\hg\edo{
1360−\MO{NewProof}\:\TC{Infer};\;
1361−\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1362−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1361+\MO{NewProof}\;\TC{Infer};\;
1362+\ttpinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1363+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
13631364\tp\gets\MO{Patterns}\\
1364−(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
1365−\vec{\MO{Elab}}\:\td'\\
1366−\MO{NewTerm}\:\vT;\;
1365+(\td', \ve') \gets\MO{Lift}\;\tp\;\td\;\ve\\
1366+\vec{\MO{Elab}}\;\td'\\
1367+\MO{NewTerm}\;\vT;\;
13671368\ttinterp{\ve'}\\
13681369\VV{rhs}\gets\MO{Term}\\
1369−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\VV{rhs})
1370+\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\VV{rhs})
13701371}
13711372}
13721373}
@@ -1449,32 +1450,32 @@ $\tp$, then splits these patterns into those necessary to type
14491450$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
14501451$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
14511452the matched expression $\ve$ in the types of $\tp_n$.
1452−$\MO{Abstract}\:\ve\:\vw\:\vp$ simply replaces any occurrence of $\vw$ in
1453+$\MO{Abstract}\;\ve\;\vw\;\vp$ simply replaces any occurrence of $\vw$ in
14531454$\vp$ with the name $\ve$.
14541455
14551456\DM{
14561457\AR{
1457−\MO{ElabClause}\:(\vx\:\ttt\:\iwith\:\ve\:\vec{\VV{pclause}})\:\mq\\
1458+\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\ve\;\vec{\VV{pclause}})\;\mq\\
14581459\hg\hg\edo{
1459−\MO{NewProof}\:\TC{Infer};\;
1460−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1461−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1460+\MO{NewProof}\;\TC{Infer};\;
1461+\ttinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1462+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
14621463\tp\gets\MO{Patterns}\\
1463−\MO{NewTerm}\:\TC{Infer};\;
1464−\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
1465−\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1466−(\tp_w,\tp_n)\:\gets\:\MO{SplitContext}\:\vW\:\tp\\
1467−\MO{TTDecl}\:(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\:\ve\:\vw'\:\tp_{n}\to\vT)\\
1468−\tc'\gets\vec{\MO{MatchWith}}\:\tp\:\ttt\:\vec{\VV{pclause}}\\
1469−\vec{\MO{Elab}}\:\tc'\\
1470−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp_{w}\:\vw'\:\tp_{n})
1464+\MO{NewTerm}\;\TC{Infer};\;
1465+\ttinterp{\DC{MkInfer}\;\_\;\ve}\\
1466+\DC{MkInfer}\;\vW\;\vw'\gets\MO{Term}\\
1467+(\tp_w,\tp_n)\;\gets\;\MO{SplitContext}\;\vW\;\tp\\
1468+\MO{TTDecl}\;(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\;\ve\;\vw'\;\tp_{n}\to\vT)\\
1469+\tc'\gets\vec{\MO{MatchWith}}\;\tp\;\ttt\;\vec{\VV{pclause}}\\
1470+\vec{\MO{Elab}}\;\tc'\\
1471+\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\vx'\;\tp_{w}\;\vw'\;\tp_{n})
14711472}
14721473\medskip\\
1473−\MO{MatchWith}\:\tp_w\:\tp_n\:\ttt\:(\vx\:\tw\:\mid\:\ve\:\VV{rhs})\:\mq\\
1474+\MO{MatchWith}\;\tp_w\;\tp_n\;\ttt\;(\vx\;\tw\;\mid\;\ve\;\VV{rhs})\;\mq\\
14741475\hg\hg\edo{
1475−\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1476−(\tp'_w,\tp'_n)\:\gets\:\MO{SplitPats}\:\tp_w\:\tp_n\:\tp'\\
1477−\RW{return}\:(\vx'\:\tp'_w\:\ve\:\tp'_{n}\:\VV{rhs})
1476+\tp'\gets\vec{\MO{Match}}\;\tw\;\ttt\\
1477+(\tp'_w,\tp'_n)\;\gets\;\MO{SplitPats}\;\tp_w\;\tp_n\;\tp'\\
1478+\RW{return}\;(\vx'\;\tp'_w\;\ve\;\tp'_{n}\;\VV{rhs})
14781479}
14791480}
14801481}
@@ -1493,7 +1494,7 @@ $\ve$ which is the same type as the scrutinee of the \texttt{with}, $\vW$.
14931494The right hand side, $\VV{rhs}$, may either return a value directly, containing
14941495\texttt{where} clauses, or be a nested \texttt{with} block. In any case, it
14951496remains unchanged.
1496−$\MO{Match}\:\vw\:\vt$ returns a list of pattern bindings containing
1497+$\MO{Match}\;\vw\;\vt$ returns a list of pattern bindings containing
14971498the variables in $\vt$ and their matches in $\vw$.
14981499The resulting matches are split, using $\MO{SplitPats}$, into matches for those
14991500variables necessary to type $\vW$ and the rest, as before.
@@ -1604,28 +1605,28 @@ In general, \texttt{class} declarations are elaborated as follows:
16041605
16051606\DM{
16061607\AR{
1607−\MO{Elab}\:(\iclass\;\piconst{\tc}\TC{C}\:(\ta\Hab\ttt)\:\iwhere\:\td)
1608+\MO{Elab}\;(\iclass\;\piconst{\tc}\TC{C}\;(\ta\Hab\ttt)\;\iwhere\;\td)
16081609\\
16091610\hg\hg
1610−\mq\:\RW{do}\:\AR{
1611+\mq\;\RW{do}\;\AR{
16111612(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1612−\MO{Elab}\:
1613−\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\
1614−\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}\\
1615−\vec{\MO{ElabMeth}}\:(\vec{\VV{meth}}\Hab\ttt)\\
1616−\vec{\MO{ElabParent}}\:\tc
1613+\MO{Elab}\;
1614+\AR{(\RW{data}\;\TC{C}\Hab(\ta\Hab\ttt)\to\Type\;\iwhere\\
1615+\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\;\ta)}\\
1616+\vec{\MO{ElabMeth}}\;(\vec{\VV{meth}}\Hab\ttt)\\
1617+\vec{\MO{ElabParent}}\;\tc
16171618}
16181619\medskip\\
1619−\MO{ElabMeth}\:(\vf\Hab\vt)\\
1620−\hg\hg\mq\:\RW{do}\:\AR{
1621−\MO{Elab}\:(\vf\Hab\TC{C}\:\ta\to\vt)\\
1622−\MO{Elab}\:(\vf\:(\DC{InstanceC}\:\vec{\VV{meth}})\:=\:\vec{\VV{meth}[\vf]})
1620+\MO{ElabMeth}\;(\vf\Hab\vt)\\
1621+\hg\hg\mq\;\RW{do}\;\AR{
1622+\MO{Elab}\;(\vf\Hab\TC{C}\;\ta\to\vt)\\
1623+\MO{Elab}\;(\vf\;(\DC{InstanceC}\;\vec{\VV{meth}})\;=\;\vec{\VV{meth}[\vf]})
16231624}
16241625\medskip\\
1625−\MO{ElabParent}\:\vc\\
1626−\hg\hg\mq\:\RW{do}\:\AR{
1627−\MO{Elab}\:(\VV{cC}\Hab\TC{C}\:\ta\to\vc)\\
1628−\MO{Elab}\:(\VV{cC}\:(\DC{InstanceC}\:\carg{\vc'}\:\vec{\VV{meth}})\:=\:\vc')
1626+\MO{ElabParent}\;\vc\\
1627+\hg\hg\mq\;\RW{do}\;\AR{
1628+\MO{Elab}\;(\VV{cC}\Hab\TC{C}\;\ta\to\vc)\\
1629+\MO{Elab}\;(\VV{cC}\;(\DC{InstanceC}\;\carg{\vc'}\;\vec{\VV{meth}})\;=\;\vc')
16291630}
16301631}
16311632}
@@ -1634,17 +1635,17 @@ In general, \texttt{class} declarations are elaborated as follows:
16341635Then \texttt{instance} declarations are elaborated as follows. One complication
16351636is that the function definitions in an \texttt{instance} declaration do not
16361637have explicit types, so we must retrieve the method types from the system state
1637−and substitute $\TC{C}\:\ttt$, using $\MO{ExpandTypes}$:
1638+and substitute $\TC{C}\;\ttt$, using $\MO{ExpandTypes}$:
16381639
16391640\DM{
16401641\AR{
1641−\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
1642−\hg\hg\mq\:\RW{do}\:\AR{
1643−(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\MO{ExpandTypes}\:\td\\
1644−\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
1645−\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
1646−\MO{Elab}\:\AR{
1647−(\FN{instanceC}\:=\:\DC{InstanceC}\;\vec{\VV{meth'}}\;\iwhere
1642+\MO{Elab}\;(\iinstance\;\piconst{\tc}\TC{C}\;\ttt\;\iwhere\;\td)\\
1643+\hg\hg\mq\;\RW{do}\;\AR{
1644+(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\MO{ExpandTypes}\;\td\\
1645+\vec{\VV{ty'}}\;=\;\vec{\VV{ty}}[\ttt/\ta]\\
1646+\MO{Elab}\;(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\;\ttt)\\
1647+\MO{Elab}\;\AR{
1648+(\FN{instanceC}\;=\;\DC{InstanceC}\;\vec{\VV{meth'}}\;\iwhere
16481649\\
16491650\hg\vec{\VV{meth'}}\Hab\vec{\VV{ty'}}\\
16501651\hg\td
@@ -1678,15 +1679,15 @@ basic primitive for proof search, and is defined as follows:
16781679
16791680\DM{
16801681\AR{
1681−\MO{Trivial}\:\mq\:
1682−\RW{do}\:\AR{
1682+\MO{Trivial}\;\mq\;
1683+\RW{do}\;\AR{
16831684 (\tv\Hab\ttt)\gets\MO{Context}\\
1684− \MO{TryAll}\:\tv
1685+ \MO{TryAll}\;\tv
16851686 }
16861687\medskip\\
1687−\MO{TryAll}\:(\vv_1,\vv_2\ldots)\:\mq\:\MO{Try}\:(\MO{Fill}\:\vv_1)\:(\MO{TryAll}\:\vv_2\ldots)
1688+\MO{TryAll}\;(\vv_1,\vv_2\ldots)\;\mq\;\MO{Try}\;(\MO{Fill}\;\vv_1)\;(\MO{TryAll}\;\vv_2\ldots)
16881689\\
1689−\MO{TryAll}\:\langle\rangle\:\mq\:\MO{Fail}
1690+\MO{TryAll}\;\langle\rangle\;\mq\;\MO{Fail}
16901691}
16911692}
16921693
@@ -1707,11 +1708,11 @@ applying every type class instance, and attempting to resolve the instance's par
17071708recursively. Given an instance $\vI$ with parameters $\ta$:
17081709
17091710\DM{
1710−\MO{TryInstance}\:(\vI\:\ta)\:\mq\:\RW{do}\;
1711+\MO{TryInstance}\;(\vI\;\ta)\;\mq\;\RW{do}\;
17111712\AR{
1712−\vec{\MO{Claim}}\:(\tx\Hab\ta)\\
1713−\ttinterp{\vI\:\tx}\\
1714−\vec{\MO{Focus}}\:\tx;\;\vec{\MO{Instance}}
1713+\vec{\MO{Claim}}\;(\tx\Hab\ta)\\
1714+\ttinterp{\vI\;\tx}\\
1715+\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
17151716}
17161717}
17171718
@@ -1719,13 +1720,13 @@ We define $\MO{Instance}$ as follows, using $\MO{AllInstances}$ to retrieve
17191720all possible type class instances in the form required by $\MO{TryInstance}$:
17201721
17211722\DM{
1722−\MO{Instance}\:\mq\:
1723−\MO{Try}\:
1723+\MO{Instance}\;\mq\;
1724+\MO{Try}\;
17241725\AR{
17251726\MO{Trivial}\\
1726−(\RW{do}\:\AR{
1727+(\RW{do}\;\AR{
17271728\ti\gets\MO{AllInstances}\\
1728−\vec{\MO{TryInstance}}\:\ti
1729+\vec{\MO{TryInstance}}\;\ti
17291730)
17301731}
17311732}
@@ -1769,9 +1770,9 @@ and $\icase$ expressions:
17691770\begin{array}{rll@{\hg}rll}
17701771\ve ::= & \ldots \\
17711772\mid & \mvar{\vx} & (\mbox{metavariable}) &
1772−\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\
1773+\mid & \icase\;\ve\;\iof\;\vec{\VV{alt}} & (\mbox{case expression}) \\
17731774\medskip\\
1774−\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\
1775+\VV{alt} ::= & \ve\;\fatarrow\;\ve & (\mbox{case alternative})\\
17751776\end{array}
17761777}
17771778}
@@ -1824,12 +1825,12 @@ Elaborating a metavariable involves adding a new top level definition which is a
18241825to all of the variables in local scope.
18251826
18261827\DM{
1827−\ttinterp{\mvar{\vx}}\:\mq\:
1828+\ttinterp{\mvar{\vx}}\;\mq\;
18281829\edo{
18291830(\tv\Hab\ttt)\gets\MO{Context}\\
18301831\vT\gets\MO{Type}\\
1831−\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vT)\\
1832−\ttinterp{\vx\:\tv}
1832+\MO{TTDecl}\;(\vx\Hab(\tv\Hab\ttt)\to\vT)\\
1833+\ttinterp{\vx\;\tv}
18331834}
18341835}
18351836
@@ -1867,14 +1868,14 @@ and elaborate it:
18671868
18681869\DM{
18691870\AR{
1870−\ttinterp{\icase\:\ve\:\iof\:\vec{\VV{alt}}}\:\mq\:
1871+\ttinterp{\icase\;\ve\;\iof\;\vec{\VV{alt}}}\;\mq\;
18711872\edo{
1872−\ttinterp{\ilet{\VV{scrutinee}}{\ve}\:\mvar{\VV{xcase}}}\\
1873+\ttinterp{\ilet{\VV{scrutinee}}{\ve}\;\mvar{\VV{xcase}}}\\
18731874(\tv\Hab\ttt)\gets\MO{Context}\\
1874−\vec{\MO{MkCase}}\:\tv\:\VV{alt}\\
1875+\vec{\MO{MkCase}}\;\tv\;\VV{alt}\\
18751876}
18761877\medskip\\
1877−\MO{MkCase}\:\tv\:(\vl\:\fatarrow\:\vr)\:\mq\:\MO{Elab}\:(\VV{xcase}\:\tv\:\vl\:=\:\vr)
1878+\MO{MkCase}\;\tv\;(\vl\;\fatarrow\;\vr)\;\mq\;\MO{Elab}\;(\VV{xcase}\;\tv\;\vl\;=\;\vr)
18781879}
18791880}
18801881