@@ -49,18 +49,18 @@ instantiating one such variable also instantiates all of its dependencies.
50\begin{array}{c}
50\begin{array}{c}
51\vb ::= \ldots
51\vb ::= \ldots
52− \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:
52+ \;\mid\; \hole{\vx}{\vt} \;\;(\mbox{hole binding}) \;\;
53− \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})
53+ \;\mid\; \guess{\vx}{\vt}{\vt} \;\;(\mbox{guess})
55−\mathsf{HoleVar}\:
55+\mathsf{HoleVar}\;
56\Rule{(\hole{\vx}{\vS})\in\Gamma}
56\Rule{(\hole{\vx}{\vS})\in\Gamma}
57{\Gamma\vdash\vx\Hab\vS}
57{\Gamma\vdash\vx\Hab\vS}
59−\mathsf{GuessVar}\:
59+\mathsf{GuessVar}\;
60\Rule{(\guess{\vx}{\vS}{\vs})\in\Gamma}
60\Rule{(\guess{\vx}{\vS}{\vs})\in\Gamma}
61{\Gamma\vdash\vx\Hab\vS}
61{\Gamma\vdash\vx\Hab\vS}
63−\mathsf{Hole}\:
63+\mathsf{Hole}\;
65\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT
65\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT
@@ -69,7 +69,7 @@ instantiating one such variable also instantiates all of its dependencies.
70%\hspace*{0.1cm}\vx\not\in\vT
70%\hspace*{0.1cm}\vx\not\in\vT
72−\mathsf{Guess}\:
72+\mathsf{Guess}\;
74\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT
74\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT
@@ -127,12 +127,12 @@ Exceptions are captured by the option type $\MO{Result}$ which
127either indicates success, or reports an error $\MO{Err}$:
127either indicates success, or reports an error $\MO{Err}$:
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}
134If any operation fails during a proof (e.g. a subterm fails to type check)
134If 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
136message $\ve$) unless otherwise handled.
136message $\ve$) unless otherwise handled.
138The \texttt{Elab} monad supports various operations for querying and updating
138The \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
172guess-bound variables.
172guess-bound variables.
174The proof state is initialised with the $\MO{NewProof}$ operation. Given a
174The 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:
178(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)
178(\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:
181The local context is initially empty, and the initial hole queue is the $\vx$ standing for
181The local context is initially empty, and the initial hole queue is the $\vx$ standing for
182the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.
182the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.
183In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
183In 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
185updates the proof state to:
185updates the proof state to:
@@ -211,21 +211,21 @@ may fail. We have the following primitive meta-operations:
211\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
211\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.
212% Focus and Unfocus don't need to be primitive, we could show in terms of
212% Focus and Unfocus don't need to be primitive, we could show in terms of
213% Get and Put
213% 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.
215%\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
215%\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
217$\Gamma$, returning its type.
217$\Gamma$, returning its type.
218$\MO{Check}$ will fail
218$\MO{Check}$ will fail
219if the expression is not well-typed.
219if 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
221$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,
221$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,
222but does not reduce definitions which are not total.
222but does not reduce definitions which are not total.
224−$\PrimUnify\:\ve_1\:\ve_2$,
224+$\PrimUnify\;\ve_1\;\ve_2$,
225which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
225which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
226holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
226holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
227to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).
227to $\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
229$\ve$, typically arising from unification.
229$\ve$, typically arising from unification.
230\end{itemize}
230\end{itemize}
@@ -233,12 +233,12 @@ $\ve$, typically arising from unification.
233Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
233Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
234and $\MO{NextHole}$
234and $\MO{NextHole}$
235operations which manipulate and inspect
235operations 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:
239−\MO{Focus}\:\vn\:=\:\RW{do}\:\AR{
239+\MO{Focus}\;\vn\;=\;\RW{do}\;\AR{
240(\vC,\Delta,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\
240(\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')\\
@@ -247,9 +247,9 @@ Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the
247end of the hole queue:
247end of the hole queue:
250−\MO{Unfocus}\:=\:\RW{do}\:\AR{
250+\MO{Unfocus}\;=\;\RW{do}\;\AR{
251(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
251(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
252−\MO{Put}\:(\vC,\Delta,\vP,\vQ;\vn)\\
252+\MO{Put}\;(\vC,\Delta,\vP,\vQ;\vn)\\
@@ -259,14 +259,14 @@ next, and $\MO{NextHole}$ returns the next hole to be solved:
262−\MO{NewHole}\:=\:\RW{do}\:\AR{
262+\MO{NewHole}\;=\;\RW{do}\;\AR{
263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
264−\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
264+\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ)\\
267−\MO{NextHole}\:=\:\RW{do}\:\AR{
267+\MO{NextHole}\;=\;\RW{do}\;\AR{
268(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
268(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
269−\MO{Return}\:\vn
269+\MO{Return}\;\vn
@@ -278,7 +278,7 @@ form:
280\PA{\A\A}{
280\PA{\A\A}{
281−\MO{Tactic}_\Gamma & \:\vec{\VV{args}} & \:\vt & \MoRet{\vt'}
281+\MO{Tactic}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\vt'}
@@ -304,40 +304,40 @@ tactic.
307−\MO{Tactic}\:\VV{tac}\:=\:\RW{do}\:\AR{
307+\MO{Tactic}\;\VV{tac}\;=\;\RW{do}\;\AR{
308\ve\Gets\MO{Term}\\
308\ve\Gets\MO{Term}\\
309\vh\Gets\MO{NextHole}\\
309\vh\Gets\MO{NextHole}\\
310−\ve'\Gets\MO{Tactic'}\:\langle\rangle\:\ve\:\VV{tac}\:\vh\\
310+\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\;\VV{tac}\;\vh\\
311−\MO{SetTerm}\:\ve'
311+\MO{SetTerm}\;\ve'
315\PA{\A\A\A}{
315\PA{\A\A\A}{
316\RW{where} \\
316\RW{where} \\
317& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)
317& \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} \\
319& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)
319& \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} \\
321& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
321& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
323−\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
323+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
324−\lam{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\lam{\vx}{\vT'})\:\ve}
324+\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve}
327& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
327& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
329−\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
329+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
330−\all{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\all{\vx}{\vT'})\:\ve}
330+\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve}
333−& \MO{Tactic'} & \Gamma & (\LET\:\vx\defq\vt\Hab\vT\SC\ve)
333+& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)
334−& \MoRet{\RW{do}\:\AR{\vt'\Gets\:\MO{Tactic'}\:\Gamma\:\vt\\
334+& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\
335−\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
335+\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
336−\LET\:\vx\defq\vt'\Hab\vT'\SC
336+\LET\;\vx\defq\vt'\Hab\vT'\SC
337−\MO{Tactic'}\:(\Gamma;\LET\:\vx\defq\vt'\Hab\vT')\:\ve}} \\
337+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve}} \\
338−& \MO{Tactic'} & \Gamma & (\vf\:\va) &
338+& \MO{Tactic'} & \Gamma & (\vf\;\va) &
339−\MoRet{\MO{Return}\:(\MO{Tactic'}\:\Gamma\:\vf)\: (\MO{Tactic'}\:\Gamma\:\va)}\\
339+\MoRet{\MO{Return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\
340−& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\:\vt}
340+& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\;\vt}
@@ -359,10 +359,10 @@ affect the solution to other unification problems. Instead,
359$\MO{PrimUnify}$ may give one of the following results:
359$\MO{PrimUnify}$ may give one of the following results:
361\begin{itemize}
361\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
363$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
363$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
364If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
364If $\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
366sub-terms in normal form.
366sub-terms in normal form.
367\end{itemize}
367\end{itemize}
@@ -381,21 +381,21 @@ resolve the existing problems with $\MO{ReUnify}$.
381%operation to update
381%operation to update
382%the proof state with new problems, and solve the old ones
382%the proof state with new problems, and solve the old ones
384−\Unify\:\ve_1\:\ve_2\:=\:\RW{do}\:
384+\Unify\;\ve_1\;\ve_2\;=\;\RW{do}\;
386−(\tx=\te,\tp)\gets\PrimUnify\:\ve_1\:\ve_2\\
386+(\tx=\te,\tp)\gets\PrimUnify\;\ve_1\;\ve_2\\
387−\vec{\MO{Subst}}\:\tx\:\te\\
387+\vec{\MO{Subst}}\;\tx\;\te\\
388−\MO{SubstProblems}\:(\tx=\te)\\
388+\MO{SubstProblems}\;(\tx=\te)\\
389(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\
389(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\
390−\vec{\MO{ReUnify}}\:\tP
390+\vec{\MO{ReUnify}}\;\tP
395−\MO{ReUnify}\:(\Gamma,\ve_1,\ve_2)\:=\:\RW{do}\:\AR{
395+\MO{ReUnify}\;(\Gamma,\ve_1,\ve_2)\;=\;\RW{do}\;\AR{
396−(\tx=\te,\tp)\Gets\PrimUnify\:\ve_1\:\ve_2\\
396+(\tx=\te,\tp)\Gets\PrimUnify\;\ve_1\;\ve_2\\
397−\vec{\MO{Subst}}\:\tx\:\te\\
397+\vec{\MO{Subst}}\;\tx\;\te\\
398−\MO{Return}\:\tp
398+\MO{Return}\;\tp
@@ -413,7 +413,7 @@ keeping $\vx$ at the head:
414\PA{\A\A}{
414\PA{\A\A}{
415\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
415\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} \\
@@ -429,10 +429,10 @@ solve other holes by unifying the expected type of $\vx$ with the type of $\vv$:
430\PA{\A\A}{
430\PA{\A\A}{
431\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
431\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
432− \MoRet{\RW{do}\:\AR{
432+ \MoRet{\RW{do}\;\AR{
433− \vT' \leftarrow \Check\:\vv\\
433+ \vT' \leftarrow \Check\;\vv\\
434− \Unify\:\vT\:\vT'\\
434+ \Unify\;\vT\;\vT'\\
435− \RW{return}\:\guess{\vx}{\vT}{\vv}\SC\ve}
435+ \RW{return}\;\guess{\vx}{\vT}{\vv}\SC\ve}
@@ -443,9 +443,9 @@ For example, consider the following proof term:
445\hole{\vA}{\Type}\SC\hole{\vk}{\Nat}\SC
445\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
448−\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys
448+\hole{\vys}{\Vect\;\vA\;(\suc\;\vk)}\SC\vys
@@ -455,9 +455,9 @@ attempts to
455$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:
455$\MO{Fill}$ it with an $\TC{Int}$ value $42$, we have:
457\begin{itemize}
457\begin{itemize}
458−\item $\Check\:42\:\mq\:\TC{Int}$
458+\item $\Check\;42\;\mq\;\TC{Int}$
459\item Unifying $\TC{Int}$ with $\vA$ (the type of $\vx$) is only possible if
459\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$.
461\end{itemize}
461\end{itemize}
@@ -466,9 +466,9 @@ Therefore the resulting proof term is:
468\hole{\vk}{\Nat}\SC
468\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
471−\hole{\vys}{\Vect\:\TC{Int}\:(\suc\:\vk)}\SC\vys
471+\hole{\vys}{\Vect\;\TC{Int}\;(\suc\;\vk)}\SC\vys
@@ -479,7 +479,7 @@ the guess is substituted into its scope:
481\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
481\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$)}}
@@ -495,9 +495,9 @@ handle failure using the $\MO{Try}$ tactic combinator:
496\PA{\A\A\A}{
496\PA{\A\A\A}{
497\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
497\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
498− \MoRet{\RW{case}\:\AR{\VV{t1}_\Gamma\:\vt\:\RW{of}\\
498+ \MoRet{\RW{case}\;\AR{\VV{t1}_\Gamma\;\vt\;\RW{of}\\
499− \MO{Success}\:\vt'\cq\MO{Success}\:\vt'\\
499+ \MO{Success}\;\vt'\cq\MO{Success}\;\vt'\\
500− \MO{Failure}\:\_\cq\VV{t2}_\Gamma\:\vt\\
500+ \MO{Failure}\;\_\cq\VV{t2}_\Gamma\;\vt\\
@@ -514,9 +514,9 @@ binding requires that the goal normalises to a function type:
515\PA{\A\A}{
515\PA{\A\A}{
516\MO{Lambda}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\vx) &
516\MO{Lambda}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\vx) &
517− \MoRet{\RW{do}\:\AR{
517+ \MoRet{\RW{do}\;\AR{
518− \all{\vy}{\vS}\SC\vT'\:\leftarrow\:\Eval\:\vT \\
518+ \all{\vy}{\vS}\SC\vT'\;\leftarrow\;\Eval\;\vT \\
519− \RW{return}\:\lam{\vn}{\vS}\SC\hole{\vx}{\vT'[\vn/\vy]}\SC\vx
519+ \RW{return}\;\lam{\vn}{\vS}\SC\hole{\vx}{\vT'[\vn/\vy]}\SC\vx
@@ -528,9 +528,9 @@ Creating a $\forall$ binding requires that the goal is a $\TC{Type}$:
529\PA{\A\A}{
529\PA{\A\A}{
530\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &
530\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &
531− \MoRet{\RW{do}\:\AR{
531+ \MoRet{\RW{do}\;\AR{
532− \Type\:\leftarrow\:\Check\:\vS\\
532+ \Type\;\leftarrow\;\Check\;\vS\\
533− \RW{return}\:\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx
533+ \RW{return}\;\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx
@@ -542,11 +542,11 @@ Creating a $\LET$ binding requires a type and a value.
543\PA{\A\A}{
543\PA{\A\A}{
544\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &
544\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &
545− \MoRet{\RW{do}\:\AR{
545+ \MoRet{\RW{do}\;\AR{
546− \Type\:\leftarrow\:\Check\:\vS\\
546+ \Type\;\leftarrow\;\Check\;\vS\\
547− \vS'\:\leftarrow\:\Check\:\vv\\
547+ \vS'\;\leftarrow\;\Check\;\vv\\
548− \Unify\:\vS\:\vS'\\
548+ \Unify\;\vS\;\vS'\\
549− \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
549+ \RW{return}\;\LET\;\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
@@ -563,7 +563,7 @@ head of the queue:
565\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
565\MO{Attack}_\Gamma & (\hole{\vx}{\vT}\SC\ve) &
566− \MoRet{\RW{do}\:\AR{
566+ \MoRet{\RW{do}\;\AR{
567 \MO{NewHole}\;\vx'\\
567 \MO{NewHole}\;\vx'\\
568 \RW{return}\;\guess{\vx}{\vT}{(\hole{\vx'}{\vT}\SC\vx')}\SC\ve}}
568 \RW{return}\;\guess{\vx}{\vT}{(\hole{\vx'}{\vT}\SC\vx')}\SC\ve}}
@@ -573,17 +573,17 @@ head of the queue:
573For example, consider the following proof term:
573For example, consider the following proof term:
576−\hole{\vx}{\va\to\vb}\SC\vx\:\ve
576+\hole{\vx}{\va\to\vb}\SC\vx\;\ve
580If we try to instantiate $\vx$ with a $\lambda$-binding $\vn$ immediately,
580If we try to instantiate $\vx$ with a $\lambda$-binding $\vn$ immediately,
581without applying $\MO{Attack}$ first, the $\lambda$ will scope over the
581without 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:
586−\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\:\ve
586+\lam{\vn}{\va}\SC\hole{\vx}{\vb}\SC\vx\;\ve
@@ -593,10 +593,10 @@ a $\lambda$ binding $\vn$, we get:
595\begin{array}{ll}
595\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
597& \hg\mbox{(after $\MO{Attack}$)}\\
597& \hg\mbox{(after $\MO{Attack}$)}\\
598−\guess{\vx}{\va\to\vb}{\lam{\vn}{\va}\SC\hole{\vx'}{\vb}\SC\vx'}\SC\vx\:\ve
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$)}
599+& \hg\mbox{(after $\MO{Lambda}\;\vn$)}
600\end{array}
600\end{array}
@@ -614,9 +614,9 @@ with the pattern variable directly:
615\PA{\A\A}{
615\PA{\A\A}{
616\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &
616\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &
617− \MoRet{\RW{do}\:\AR{
617+ \MoRet{\RW{do}\;\AR{
618− \MO{PatBind}\:(\vn\Hab\vT)\\
618+ \MO{PatBind}\;(\vn\Hab\vT)\\
619− \RW{return}\:\ve[\vn/\vx]
619+ \RW{return}\;\ve[\vn/\vx]
@@ -635,7 +635,7 @@ complete term by refining a proof state, let us consider the following
637\FN{id}\Hab\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
637\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
@@ -647,9 +647,9 @@ the goal type.
650−\MO{MkId}\:\mq\:\RW{do}\:
650+\MO{MkId}\;\mq\;\RW{do}\;
652− \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
652+ \MO{NewProof}\;\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
653 \MO{Tactic}\;\MO{Attack} \\
653 \MO{Tactic}\;\MO{Attack} \\
654 \MO{Tactic}\;(\MO{Lambda}\;\vA) \\
654 \MO{Tactic}\;(\MO{Lambda}\;\vA) \\
655 \MO{Tactic}\;\MO{Attack} \\
655 \MO{Tactic}\;\MO{Attack} \\
@@ -683,7 +683,7 @@ the goal type.
684\langle\vh_0,\vx\rangle\\
684\langle\vh_0,\vx\rangle\\
686−\MO{Lambda}\:\vA &
686+\MO{Lambda}\;\vA &
687\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
687\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
688\underline{
688\underline{
689\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
689\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
@@ -706,7 +706,7 @@ the goal type.
707\langle\vh_1,\vh_0,\vx\rangle\\
707\langle\vh_1,\vh_0,\vx\rangle\\
709−\MO{Lambda}\:\va &
709+\MO{Lambda}\;\va &
710\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
710\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
711\lam{\vA}{\Type}\SC
711\lam{\vA}{\Type}\SC
712\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
712\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
@@ -721,7 +721,7 @@ the goal type.
722\langle\vh_1,\vh_0,\vx\rangle\\
722\langle\vh_1,\vh_0,\vx\rangle\\
724−\MO{Fill}\:\va &
724+\MO{Fill}\;\va &
725\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
725\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
726\lam{\vA}{\Type}\SC
726\lam{\vA}{\Type}\SC
@@ -807,19 +807,19 @@ a Coq proof script.
810−\MO{MkIdType}\:\mq\:\RW{do}\;
810+\MO{MkIdType}\;\mq\;\RW{do}\;
812− \MO{NewProof}\:\Type\\
812+ \MO{NewProof}\;\Type\\
813− \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Type) ;
813+ \MO{Attack} ; \MO{Pi}\;(\vA\Hab\Type) ;
814− \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\
814+ \MO{Attack} ; \MO{Pi}\;(\va\Hab\vA) \\
815 \MO{Fill}\;\vA \\
815 \MO{Fill}\;\vA \\
816 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\
816 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\
817 \MO{Term}
817 \MO{Term}
819 \medskip\\
819 \medskip\\
820−\MO{MkId}\:\mq\:\RW{do}\;
820+\MO{MkId}\;\mq\;\RW{do}\;
822− \vt\:\leftarrow\:\MO{MkIdType}; \MO{NewProof}\:\vt\\
822+ \vt\;\leftarrow\;\MO{MkIdType}; \MO{NewProof}\;\vt\\
823 \MO{Attack} ; \MO{Lambda}\;\vA ;
823 \MO{Attack} ; \MO{Lambda}\;\vA ;
824 \MO{Attack} ; \MO{Lambda}\;\va \\
824 \MO{Attack} ; \MO{Lambda}\;\va \\
825 \MO{Fill}\;\va \\
825 \MO{Fill}\;\va \\
@@ -928,11 +928,11 @@ are given explicitly, the application must be expanded.
928\begin{array}{rll@{\hg}rll}
928\begin{array}{rll@{\hg}rll}
929\ve ::= & \vc & (\mbox{constant}) &
929\ve ::= & \vc & (\mbox{constant}) &
930\mid & \vx & (\mbox{variable}) \\
930\mid & \vx & (\mbox{variable}) \\
931−\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
931+\mid & \ilam{\vx}\;\ve & (\mbox{lambda abstraction}) &
932−\mid & \ve\:\ta & (\mbox{function application}) \\
932+\mid & \ve\;\ta & (\mbox{function application}) \\
933−\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) &
933+\mid & \ilet{\vx}{\ve}\;\ve & (\mbox{let binding}) &
934\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
934\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}) &
936%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
936%\mid & \mvar{\vx} & (\mbox{metavariable}) \\
937\mid & \_ & (\mbox{placeholder})
937\mid & \_ & (\mbox{placeholder})
938\end{array}
938\end{array}
@@ -971,9 +971,9 @@ are given explicitly, the application must be expanded.
971\begin{array}{ll}
971\begin{array}{ll}
972\begin{array}{rll}
972\begin{array}{rll}
973\VV{pclause} ::= &
973\VV{pclause} ::= &
974−\vx\:\ttt\:[\ibar\;\te]\mbox{\texttt{ = }}\ve \hg[\iwhere\;\td]\\
974+\vx\;\ttt\;[\ibar\;\te]\mbox{\texttt{ = }}\ve \hg[\iwhere\;\td]\\
975\mid & \AR{
975\mid & \AR{
976−\vx\:\ttt\:[\ibar\;\te]\;\iwith\;\ve\\
976+\vx\;\ttt\;[\ibar\;\te]\;\iwith\;\ve\\
977\hg\vec{\VV{pclause}}
977\hg\vec{\VV{pclause}}
979\end{array}
979\end{array}
@@ -984,7 +984,7 @@ are given explicitly, the application must be expanded.
984\medskip\\
984\medskip\\
985\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td
985\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td
987−\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td
987+\VV{idecl} ::= & \iinstance\;[\VV{constr}]\;\vx\;\ttt\;\iwhere\;\td
988\end{array}
988\end{array}
989\end{array}
989\end{array}
@@ -997,8 +997,8 @@ and declaration syntax given in Figure \ref{idrismd}.
997\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
997\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
998tuple syntax, \texttt{do}-notation or infix operators --- and with implicit
998tuple syntax, \texttt{do}-notation or infix operators --- and with implicit
999arguments in types bound explicitly
999arguments in types bound explicitly
1000−(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\:\va\:\vn$
1000+(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$
1001−instead of simply $\Vect\:\va\:\vn$).
1001+instead of simply $\Vect\;\va\;\vn$).
1002Note that we separate implicit and type constraint bindings, to ensure that they
1002Note that we separate implicit and type constraint bindings, to ensure that they
1003only appear in top level declarations.
1003only appear in top level declarations.
1004It is in general straightforward to
1004It is in general straightforward to
@@ -1032,7 +1032,7 @@ has already been set up, which means that elaboration can always be
1032are building.
1032are building.
1034In all cases except the elaboration of variables and constantes,
1034In all cases except the elaboration of variables and constantes,
1035−$\ttpinterp{\vx}\:=\:\ttinterp{\vx}$.
1035+$\ttpinterp{\vx}\;=\;\ttinterp{\vx}$.
1037\subsubsection{Elaborating variables and constants}
1037\subsubsection{Elaborating variables and constants}
@@ -1042,8 +1042,8 @@ the \MO{Fill} tactic:
1045−\ttinterp{\vx}\:\mq\:\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve}\\
1045+\ttinterp{\vx}\;\mq\;\RW{do}\;\MO{Fill}\;\vx;\;\MO{Solve}\\
1046−\ttinterp{\vc}\:\mq\:\RW{do}\:\MO{Fill}\:\vc;\:\MO{Solve}\\
1046+\ttinterp{\vc}\;\mq\;\RW{do}\;\MO{Fill}\;\vc;\;\MO{Solve}\\
@@ -1059,9 +1059,9 @@ context, we assume that attempting to elaborate a variable which does not type
1059check means that the variable is a pattern variable:
1059check means that the variable is a pattern variable:
1062−\ttpinterp{\vx}\:\mq\:
1062+\ttpinterp{\vx}\;\mq\;
1063−\MO{Try}\:\AR{(\RW{do}\:\MO{Fill}\:\vx;\:\MO{Solve})\\
1063+\MO{Try}\;\AR{(\RW{do}\;\MO{Fill}\;\vx;\;\MO{Solve})\\
1064−(\MO{Pat}\:\vx)
1064+(\MO{Pat}\;\vx)
@@ -1070,13 +1070,14 @@ solve by unification. In this case, we simply move on to the next hole in the qu
1070the current hole to the end of the queue with $\MO{Unfocus}$:
1070the current hole to the end of the queue with $\MO{Unfocus}$:
1073−\ttinterp{\_}\:\mq\:\MO{Unfocus}
1073+\ttinterp{\_}\;\mq\;\MO{Unfocus}
1076−On encountering a placeholder, our assumption is that unification will eventually solve
1076+On encountering a placeholder, our assumption is that unification will
1077−the hole. At the end of elaboration, any holes remaining unsolved on the left hand side
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
1078−become pattern variables. If there are any unsolved on the right hand side, elaboration
1079+unsolved on the right hand side, elaboration is incomplete and an error will
1079−fails.
1080+be reported when the resulting term is type checked.
1081\subsubsection{Elaborating bindings}
1082\subsubsection{Elaborating bindings}
@@ -1085,10 +1086,10 @@ $\MO{Lambda}$ tactic, which will fail if the goal is not a function type. We
1085then elaborate the scope and $\MO{Solve}$, which discharges the $\MO{Attack}$:
1086then elaborate the scope and $\MO{Solve}$, which discharges the $\MO{Attack}$:
1088−\ttinterp{\ilam{\vx}\ve}\:\mq\:
1089+\ttinterp{\ilam{\vx}\ve}\;\mq\;
1089−\RW{do}\:
1090+\RW{do}\;
1091−\MO{Attack};\;\MO{Lambda}\:\vx\\
1092+\MO{Attack};\;\MO{Lambda}\;\vx\\
1092\ttinterp{\ve}\\
1093\ttinterp{\ve}\\
1093\MO{Solve}
1094\MO{Solve}
@@ -1108,12 +1109,12 @@ scope of the binding.
1111−\ttinterp{\piexp{\vx}{\vt}\ve}\:\mq\:
1112+\ttinterp{\piexp{\vx}{\vt}\ve}\;\mq\;
1112−\RW{do}\:
1113+\RW{do}\;
1114−\MO{Attack};\;\MO{Claim}\:(\vX\Hab\Type)\\
1115+\MO{Attack};\;\MO{Claim}\;(\vX\Hab\Type)\\
1115−\MO{Pi}\:(\vx\Hab\vX)\\
1116+\MO{Pi}\;(\vx\Hab\vX)\\
1116−\MO{Focus}\:\vX\\
1117+\MO{Focus}\;\vX\\
1117\ttinterp{\vt};\;
1118\ttinterp{\vt};\;
1118\ttinterp{\ve}\\
1119\ttinterp{\ve}\\
1119\MO{Solve}
1120\MO{Solve}
@@ -1134,13 +1135,13 @@ if elaborating the scope is successful, unification will solve the claimed varia
1134$\vV$ and $\vX$.
1135$\vV$ and $\vX$.
1137−\ttinterp{\ilet{\vx}{\vv}\:{\ve}}\:\mq\:\RW{do}\:
1138+\ttinterp{\ilet{\vx}{\vv}\;{\ve}}\;\mq\;\RW{do}\;
1139\MO{Attack};\;
1140\MO{Attack};\;
1140−\MO{Claim}\:(\vX\Hab\Type);\;
1141+\MO{Claim}\;(\vX\Hab\Type);\;
1141−\MO{Claim}\:(\vV\Hab\vX)\\
1142+\MO{Claim}\;(\vV\Hab\vX)\\
1142−\MO{Let}\:(\vx\Hab\vX\defq\vV)\\
1143+\MO{Let}\;(\vx\Hab\vX\defq\vV)\\
1143−\MO{Focus}\:\vV\\
1144+\MO{Focus}\;\vV\\
1144\ttinterp{\vv};\;
1145\ttinterp{\vv};\;
1145\ttinterp{\ve}
1146\ttinterp{\ve}
@@ -1158,7 +1159,7 @@ In the first case, the elaborator must expand the application to include implici
1158For example \texttt{vAdd xs ys} is expanded to
1159For example \texttt{vAdd xs ys} is expanded to
1159\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments
1160\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments
1160\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation
1161\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
1162arguments supplied by the programmer $\ta$, returns a new argument list
1163arguments supplied by the programmer $\ta$, returns a new argument list
1163$\ta'$ with implicit and type class arguments added. Each value in
1164$\ta'$ with implicit and type class arguments added. Each value in
1164$\ta'$ is paired with an explicit name for the argument.
1165$\ta'$ is paired with an explicit name for the argument.
@@ -1172,17 +1173,17 @@ forms:
1175−\MO{Unify}_\Gamma\;\vf\:\TC{Int}\\
1176+\MO{Unify}_\Gamma\;\vf\;\TC{Int}\\
1176−\MO{Unify}_\Gamma\;(\vf\:\vx)\:\TC{Int}\\
1177+\MO{Unify}_\Gamma\;(\vf\;\vx)\;\TC{Int}\\
1177−\MO{Unify}_\Gamma\;(\vf\:\vx)\:(\vg\:\vx)\\
1178+\MO{Unify}_\Gamma\;(\vf\;\vx)\;(\vg\;\vx)\\
1181The first problem has a solution: $\vf=\TC{Int}$. The second and third problems
1182The first problem has a solution: $\vf=\TC{Int}$. The second and third problems
1182have no solution without further information. In the second case, we cannot
1183have no solution without further information. In the second case, we cannot
1183conclude anything about $\vf$ or $\vx$ just from knowing that
1184conclude 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+$\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
1186+argument position, we cannot conclude that $\vf\;=\;\vg$ in general as a
1188Once $\vf$ or $\vg$ is solved in some other way, perhaps by being given
1189Once $\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
1198built-in $\MO{Instance}$ tactic.
1199built-in $\MO{Instance}$ tactic.
1201−\ttinterp{\vx\:\ta}\:\mq\:
1202+\ttinterp{\vx\;\ta}\;\mq\;
1203−\RW{do}\:
1204+\RW{do}\;
1205−(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
1206+(\tn,\tv)\;\gets\;\MO{Expand}\;\vx\;\ta\\
1206−\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
1207+\vec{\MO{Claim}}\;(\tn\Hab\tT)\\
1207−\MO{Fill}\:\vx\:\tn\\
1208+\MO{Fill}\;\vx\;\tn\\
1208−\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
1209+\vec{\MO{Focus}}\;\tn;\;\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
1209\MO{Solve} \\
1210\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$)}
@@ -1224,12 +1225,12 @@ applied. Since elaboration is type directed, however, there must be an
1224appropriate type for the function.
1225appropriate type for the function.
1227−\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
1228+\ttinterp{\ve\;\va}\;\mq\;\RW{do}\;
1229−\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\
1230+\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{Claim}\;(\vf\Hab\vA\to\vB);\;\MO{Claim}\;(\vs\Hab\vA)\\
1231−\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
1232+\MO{Focus}\;\vf;\;\ttinterp{\ve}\\
1232−\MO{Focus}\:\vs;\;\ttinterp{\va}\\
1233+\MO{Focus}\;\vs;\;\ttinterp{\va}\\
@@ -1244,7 +1245,7 @@ relative to the system state (see Section \ref{sect:sysstate}) and has access to
1244current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate
1245current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate
1245\IdrisM{} type, function and class declarations into \TT{} declarations.
1246\IdrisM{} type, function and class declarations into \TT{} declarations.
1247−\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
1248+\newcommand{\edo}[1]{\RW{do}\;\AR{#1}}
1249\subsubsection{Elaborating Type Declarations}
1250\subsubsection{Elaborating Type Declarations}
@@ -1253,11 +1254,11 @@ translating the \IdrisM{} type to a \TT{} type, then adding the resulting type
1253as a \TT{} declaration:
1254as a \TT{} declaration:
1256−\MO{Elab}\:(\vx\Hab\vt)\:\mq
1257+\MO{Elab}\;(\vx\Hab\vt)\;\mq
1257−\:\edo{\MO{NewProof}\:\Type\\
1258+\;\edo{\MO{NewProof}\;\Type\\
1258 \ttinterp{\vt}\\
1259 \ttinterp{\vt}\\
1259 \vt'\gets\MO{Term}\\
1260 \vt'\gets\MO{Term}\\
1260− \MO{TTDecl}\:(\vx\Hab\vt')
1261+ \MO{TTDecl}\;(\vx\Hab\vt')
1263The final $\MO{TTDecl}$ takes the result of elaboration, type checks it,
1264The final $\MO{TTDecl}$ takes the result of elaboration, type checks it,
@@ -1274,20 +1275,20 @@ adds a \TT{} data declaration.
1277−\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
1278+\MO{Elab}\;(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\
1278−\hg\hg\mq\:\edo{\MO{NewProof}\:\Type\\
1279+\hg\hg\mq\;\edo{\MO{NewProof}\;\Type\\
1279 \ttinterp{\vt}\\
1280 \ttinterp{\vt}\\
1280 \vt'\gets\MO{Term}\\
1281 \vt'\gets\MO{Term}\\
1281− \MO{TTDecl}\:(\vx\Hab\vt')\\
1282+ \MO{TTDecl}\;(\vx\Hab\vt')\\
1282− \tc'\gets\vec{\MO{ElabCon}}\:\tc\\
1283+ \tc'\gets\vec{\MO{ElabCon}}\;\tc\\
1283− \MO{TTDecl}\:(\Data\:\vx\Hab\vt'\:\Where\:\tc')
1284+ \MO{TTDecl}\;(\Data\;\vx\Hab\vt'\;\Where\;\tc')
1286−\MO{ElabCon}\:(\vx\Hab\vt)\\
1287+\MO{ElabCon}\;(\vx\Hab\vt)\\
1287−\hg\hg\mq\: \edo{\MO{NewProof}\:\Type\\
1288+\hg\hg\mq\; \edo{\MO{NewProof}\;\Type\\
1288 \ttinterp{\vt}\\
1289 \ttinterp{\vt}\\
1289 \vt'\gets\MO{Term}\\
1290 \vt'\gets\MO{Term}\\
1290− \RW{return}\:(\vx\Hab\vt')
1291+ \RW{return}\;(\vx\Hab\vt')
@@ -1300,7 +1301,7 @@ to the global context, such as definitions in $\iwhere$ clauses.
1300First, let us consider the simplest case, with no $\iwhere$ clause:
1301First, let us consider the simplest case, with no $\iwhere$ clause:
1303−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
1304+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;?
1306How does the left hand side get elaborated, given that elaboration is type directed, and
1307How does the left hand side get elaborated, given that elaboration is type directed, and
@@ -1312,21 +1313,21 @@ a type $\TC{Infer}$:
1312\Data\hg\TC{Infer}\Hab\Type\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Type}\SC\va\to\TC{Infer}
1313\Data\hg\TC{Infer}\Hab\Type\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Type}\SC\va\to\TC{Infer}
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
1316extracting the value and unified type when complete.
1317extracting the value and unified type when complete.
1320−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:\\
1321+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;\\
1321\hg\hg\edo{
1322\hg\hg\edo{
1322−\MO{NewProof}\:\TC{Infer};\;
1323+\MO{NewProof}\;\TC{Infer};\;
1323−\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1324+\ttpinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1324−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1325+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
1325\tp\gets\MO{Patterns}\\
1326\tp\gets\MO{Patterns}\\
1326−\MO{NewTerm}\:\vT;\;
1327+\MO{NewTerm}\;\vT;\;
1327\ttinterp{\ve}\\
1328\ttinterp{\ve}\\
1328\VV{rhs}\gets\MO{Term}\\
1329\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})
@@ -1340,10 +1341,10 @@ the clauses and adding the resulting collection to \TT{}.
1343−\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
1344+\MO{Elab}\;\vec{\VV{pclause}}\;\mq\;
1345−\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
1346+\tc\gets\vec{\MO{ElabClause}}\;\vec{\VV{pclause}}\\
1346−\vec{\MO{TTDecl}}\:\tc
1347+\vec{\MO{TTDecl}}\;\tc
@@ -1355,18 +1356,18 @@ which are then recursively elaborated before the right hand side.
1358−\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve\:\iwhere\:\td)\:\mq\:\\
1359+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve\;\iwhere\;\td)\;\mq\;\\
1359\hg\hg\edo{
1360\hg\hg\edo{
1360−\MO{NewProof}\:\TC{Infer};\;
1361+\MO{NewProof}\;\TC{Infer};\;
1361−\ttpinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1362+\ttpinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1362−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1363+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
1363\tp\gets\MO{Patterns}\\
1364\tp\gets\MO{Patterns}\\
1364−(\td', \ve') \gets\MO{Lift}\:\tp\:\td\:\ve\\
1365+(\td', \ve') \gets\MO{Lift}\;\tp\;\td\;\ve\\
1365−\vec{\MO{Elab}}\:\td'\\
1366+\vec{\MO{Elab}}\;\td'\\
1366−\MO{NewTerm}\:\vT;\;
1367+\MO{NewTerm}\;\vT;\;
1367\ttinterp{\ve'}\\
1368\ttinterp{\ve'}\\
1368\VV{rhs}\gets\MO{Term}\\
1369\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})
@@ -1449,32 +1450,32 @@ $\tp$, then splits these patterns into those necessary to type
1449$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
1450$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
1450$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
1451$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
1451the matched expression $\ve$ in the types of $\tp_n$.
1452the 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
1453$\vp$ with the name $\ve$.
1454$\vp$ with the name $\ve$.
1457−\MO{ElabClause}\:(\vx\:\ttt\:\iwith\:\ve\:\vec{\VV{pclause}})\:\mq\\
1458+\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\ve\;\vec{\VV{pclause}})\;\mq\\
1458\hg\hg\edo{
1459\hg\hg\edo{
1459−\MO{NewProof}\:\TC{Infer};\;
1460+\MO{NewProof}\;\TC{Infer};\;
1460−\ttinterp{\DC{MkInfer}\:\_\:(\vx\:\ttt)}\\
1461+\ttinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
1461−\DC{MkInfer}\:\vT\:\VV{lhs}\gets\MO{Term}\\
1462+\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
1462\tp\gets\MO{Patterns}\\
1463\tp\gets\MO{Patterns}\\
1463−\MO{NewTerm}\:\TC{Infer};\;
1464+\MO{NewTerm}\;\TC{Infer};\;
1464−\ttinterp{\DC{MkInfer}\:\_\:\ve}\\
1465+\ttinterp{\DC{MkInfer}\;\_\;\ve}\\
1465−\DC{MkInfer}\:\vW\:\vw'\gets\MO{Term}\\
1466+\DC{MkInfer}\;\vW\;\vw'\gets\MO{Term}\\
1466−(\tp_w,\tp_n)\:\gets\:\MO{SplitContext}\:\vW\:\tp\\
1467+(\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+\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+\tc'\gets\vec{\MO{MatchWith}}\;\tp\;\ttt\;\vec{\VV{pclause}}\\
1469−\vec{\MO{Elab}}\:\tc'\\
1470+\vec{\MO{Elab}}\;\tc'\\
1470−\RW{return}\:(\RW{var}\:\tp\SC\VV{lhs}\:=\:\vx'\:\tp_{w}\:\vw'\:\tp_{n})
1471+\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\vx'\;\tp_{w}\;\vw'\;\tp_{n})
1472\medskip\\
1473\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\\
1474\hg\hg\edo{
1475\hg\hg\edo{
1475−\tp'\gets\vec{\MO{Match}}\:\tw\:\ttt\\
1476+\tp'\gets\vec{\MO{Match}}\;\tw\;\ttt\\
1476−(\tp'_w,\tp'_n)\:\gets\:\MO{SplitPats}\:\tp_w\:\tp_n\:\tp'\\
1477+(\tp'_w,\tp'_n)\;\gets\;\MO{SplitPats}\;\tp_w\;\tp_n\;\tp'\\
1477−\RW{return}\:(\vx'\:\tp'_w\:\ve\:\tp'_{n}\:\VV{rhs})
1478+\RW{return}\;(\vx'\;\tp'_w\;\ve\;\tp'_{n}\;\VV{rhs})
@@ -1493,7 +1494,7 @@ $\ve$ which is the same type as the scrutinee of the \texttt{with}, $\vW$.
1493The right hand side, $\VV{rhs}$, may either return a value directly, containing
1494The right hand side, $\VV{rhs}$, may either return a value directly, containing
1494\texttt{where} clauses, or be a nested \texttt{with} block. In any case, it
1495\texttt{where} clauses, or be a nested \texttt{with} block. In any case, it
1495remains unchanged.
1496remains 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
1497the variables in $\vt$ and their matches in $\vw$.
1498the variables in $\vt$ and their matches in $\vw$.
1498The resulting matches are split, using $\MO{SplitPats}$, into matches for those
1499The resulting matches are split, using $\MO{SplitPats}$, into matches for those
1499variables necessary to type $\vW$ and the rest, as before.
1500variables necessary to type $\vW$ and the rest, as before.
@@ -1604,28 +1605,28 @@ In general, \texttt{class} declarations are elaborated as follows:
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)
1610−\mq\:\RW{do}\:\AR{
1611+\mq\;\RW{do}\;\AR{
1611(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1612(\vec{\VV{meth}}\Hab\ttt)\gets\td\\
1612−\MO{Elab}\:
1613+\MO{Elab}\;
1613−\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\
1614+\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+\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\;\ta)}\\
1615−\vec{\MO{ElabMeth}}\:(\vec{\VV{meth}}\Hab\ttt)\\
1616+\vec{\MO{ElabMeth}}\;(\vec{\VV{meth}}\Hab\ttt)\\
1616−\vec{\MO{ElabParent}}\:\tc
1617+\vec{\MO{ElabParent}}\;\tc
1618\medskip\\
1619\medskip\\
1619−\MO{ElabMeth}\:(\vf\Hab\vt)\\
1620+\MO{ElabMeth}\;(\vf\Hab\vt)\\
1620−\hg\hg\mq\:\RW{do}\:\AR{
1621+\hg\hg\mq\;\RW{do}\;\AR{
1621−\MO{Elab}\:(\vf\Hab\TC{C}\:\ta\to\vt)\\
1622+\MO{Elab}\;(\vf\Hab\TC{C}\;\ta\to\vt)\\
1622−\MO{Elab}\:(\vf\:(\DC{InstanceC}\:\vec{\VV{meth}})\:=\:\vec{\VV{meth}[\vf]})
1623+\MO{Elab}\;(\vf\;(\DC{InstanceC}\;\vec{\VV{meth}})\;=\;\vec{\VV{meth}[\vf]})
1624\medskip\\
1625\medskip\\
1625−\MO{ElabParent}\:\vc\\
1626+\MO{ElabParent}\;\vc\\
1626−\hg\hg\mq\:\RW{do}\:\AR{
1627+\hg\hg\mq\;\RW{do}\;\AR{
1627−\MO{Elab}\:(\VV{cC}\Hab\TC{C}\:\ta\to\vc)\\
1628+\MO{Elab}\;(\VV{cC}\Hab\TC{C}\;\ta\to\vc)\\
1628−\MO{Elab}\:(\VV{cC}\:(\DC{InstanceC}\:\carg{\vc'}\:\vec{\VV{meth}})\:=\:\vc')
1629+\MO{Elab}\;(\VV{cC}\;(\DC{InstanceC}\;\carg{\vc'}\;\vec{\VV{meth}})\;=\;\vc')
@@ -1634,17 +1635,17 @@ In general, \texttt{class} declarations are elaborated as follows:
1634Then \texttt{instance} declarations are elaborated as follows. One complication
1635Then \texttt{instance} declarations are elaborated as follows. One complication
1635is that the function definitions in an \texttt{instance} declaration do not
1636is that the function definitions in an \texttt{instance} declaration do not
1636have explicit types, so we must retrieve the method types from the system state
1637have 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}$:
1641−\MO{Elab}\:(\iinstance\;\piconst{\tc}\TC{C}\:\ttt\:\iwhere\:\td)\\
1642+\MO{Elab}\;(\iinstance\;\piconst{\tc}\TC{C}\;\ttt\;\iwhere\;\td)\\
1642−\hg\hg\mq\:\RW{do}\:\AR{
1643+\hg\hg\mq\;\RW{do}\;\AR{
1643−(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\MO{ExpandTypes}\:\td\\
1644+(\vec{\VV{meth}}, \vec{\VV{ty}})\gets\MO{ExpandTypes}\;\td\\
1644−\vec{\VV{ty'}}\:=\:\vec{\VV{ty}}[\ttt/\ta]\\
1645+\vec{\VV{ty'}}\;=\;\vec{\VV{ty}}[\ttt/\ta]\\
1645−\MO{Elab}\:(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\:\ttt)\\
1646+\MO{Elab}\;(\FN{instanceC}\Hab\piconst{\tc}\TC{C}\;\ttt)\\
1646−\MO{Elab}\:\AR{
1647+\MO{Elab}\;\AR{
1647−(\FN{instanceC}\:=\:\DC{InstanceC}\;\vec{\VV{meth'}}\;\iwhere
1648+(\FN{instanceC}\;=\;\DC{InstanceC}\;\vec{\VV{meth'}}\;\iwhere
1649\hg\vec{\VV{meth'}}\Hab\vec{\VV{ty'}}\\
1650\hg\vec{\VV{meth'}}\Hab\vec{\VV{ty'}}\\
@@ -1678,15 +1679,15 @@ basic primitive for proof search, and is defined as follows:
1681−\MO{Trivial}\:\mq\:
1682+\MO{Trivial}\;\mq\;
1682−\RW{do}\:\AR{
1683+\RW{do}\;\AR{
1683 (\tv\Hab\ttt)\gets\MO{Context}\\
1684 (\tv\Hab\ttt)\gets\MO{Context}\\
1684− \MO{TryAll}\:\tv
1685+ \MO{TryAll}\;\tv
1686\medskip\\
1687\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)
1689−\MO{TryAll}\:\langle\rangle\:\mq\:\MO{Fail}
1690+\MO{TryAll}\;\langle\rangle\;\mq\;\MO{Fail}
@@ -1707,11 +1708,11 @@ applying every type class instance, and attempting to resolve the instance's par
1707recursively. Given an instance $\vI$ with parameters $\ta$:
1708recursively. Given an instance $\vI$ with parameters $\ta$:
1710−\MO{TryInstance}\:(\vI\:\ta)\:\mq\:\RW{do}\;
1711+\MO{TryInstance}\;(\vI\;\ta)\;\mq\;\RW{do}\;
1712−\vec{\MO{Claim}}\:(\tx\Hab\ta)\\
1713+\vec{\MO{Claim}}\;(\tx\Hab\ta)\\
1713−\ttinterp{\vI\:\tx}\\
1714+\ttinterp{\vI\;\tx}\\
1714−\vec{\MO{Focus}}\:\tx;\;\vec{\MO{Instance}}
1715+\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
@@ -1719,13 +1720,13 @@ We define $\MO{Instance}$ as follows, using $\MO{AllInstances}$ to retrieve
1719all possible type class instances in the form required by $\MO{TryInstance}$:
1720all possible type class instances in the form required by $\MO{TryInstance}$:
1722−\MO{Instance}\:\mq\:
1723+\MO{Instance}\;\mq\;
1723−\MO{Try}\:
1724+\MO{Try}\;
1725\MO{Trivial}\\
1726\MO{Trivial}\\
1726−(\RW{do}\:\AR{
1727+(\RW{do}\;\AR{
1727\ti\gets\MO{AllInstances}\\
1728\ti\gets\MO{AllInstances}\\
1728−\vec{\MO{TryInstance}}\:\ti
1729+\vec{\MO{TryInstance}}\;\ti
@@ -1769,9 +1770,9 @@ and $\icase$ expressions:
1769\begin{array}{rll@{\hg}rll}
1770\begin{array}{rll@{\hg}rll}
1770\ve ::= & \ldots \\
1771\ve ::= & \ldots \\
1771\mid & \mvar{\vx} & (\mbox{metavariable}) &
1772\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}) \\
1773\medskip\\
1774\medskip\\
1774−\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\
1775+\VV{alt} ::= & \ve\;\fatarrow\;\ve & (\mbox{case alternative})\\
1775\end{array}
1776\end{array}
@@ -1824,12 +1825,12 @@ Elaborating a metavariable involves adding a new top level definition which is a
1824to all of the variables in local scope.
1825to all of the variables in local scope.
1827−\ttinterp{\mvar{\vx}}\:\mq\:
1828+\ttinterp{\mvar{\vx}}\;\mq\;
1829(\tv\Hab\ttt)\gets\MO{Context}\\
1830(\tv\Hab\ttt)\gets\MO{Context}\\
1830\vT\gets\MO{Type}\\
1831\vT\gets\MO{Type}\\
1831−\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vT)\\
1832+\MO{TTDecl}\;(\vx\Hab(\tv\Hab\ttt)\to\vT)\\
1832−\ttinterp{\vx\:\tv}
1833+\ttinterp{\vx\;\tv}
@@ -1867,14 +1868,14 @@ and elaborate it:
1870−\ttinterp{\icase\:\ve\:\iof\:\vec{\VV{alt}}}\:\mq\:
1871+\ttinterp{\icase\;\ve\;\iof\;\vec{\VV{alt}}}\;\mq\;
1872−\ttinterp{\ilet{\VV{scrutinee}}{\ve}\:\mvar{\VV{xcase}}}\\
1873+\ttinterp{\ilet{\VV{scrutinee}}{\ve}\;\mvar{\VV{xcase}}}\\
1873(\tv\Hab\ttt)\gets\MO{Context}\\
1874(\tv\Hab\ttt)\gets\MO{Context}\\
1874−\vec{\MO{MkCase}}\:\tv\:\VV{alt}\\
1875+\vec{\MO{MkCase}}\;\tv\;\VV{alt}\\
1876\medskip\\
1877\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)