@@ -34,7 +34,7 @@ Holes stand for the parts of programs which have not yet been
3434instantiated; this largely follows the Oleg development
3535calculus~\cite{McBride1999}.
3636
37−The basic idea is to extend the syntax for binders with a \remph{hole}
37+The idea is to extend the syntax for binders with a \remph{hole}
3838binding and a \remph{guess} binding.
3939These extensions are given in Figure \ref{ttdev}.
4040The \remph{guess} binding is
@@ -101,7 +101,7 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
101101\item Unsolved unification problems, $\vP$
102102\begin{itemize}
103103\item These take the form $(\Gamma,\ve_1,\ve_2)$, i.e. the context in which
104−the problem is run, and the expressions to be unified.
104+the problem is to be solved, and the expressions to be unified.
105105\end{itemize}
106106\item A hole queue, $\vQ$
107107%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
@@ -110,7 +110,7 @@ the problem is run, and the expressions to be unified.
110110The \remph{hole queue} is a priority queue of names of hole and guess binders
111111$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
112112in the proof term ---
113−ensuring that each bound name is unique. Holes refer to \remph{sub goals}
113+ensuring that each bound name is unique. Holes refer to \remph{sub-goals}
114114in the proof. As a proof develops, unification problems arising from unsolved
115115holes may be introduced, and may be solved when those holes are instantiated.
116116When the hole queue is empty, and there are no remaining unification
@@ -130,7 +130,7 @@ either indicates success, or reports an error $\MO{Err}$:
130130}
131131
132132\noindent
133−If any operation fails during a proof (e.g. a sub term fails to type check)
133+If any operation fails during a proof (e.g. a sub-term fails to type check)
134134then the entire proof fails (i.e. returns $\MO{Failure}\;\ve$ with some error
135135message $\ve$) unless otherwise handled.
136136
@@ -144,22 +144,21 @@ distracted by implementation details. These meta-operations include:
144144\item \demph{Queries} which retrieve values from the proof state, without modifying
145145the state. For example, we can:
146146\begin{itemize}
147−\item Get the type of the current sub goal ($\MO{Type}$).
148−\item Get the current proof term ($\MO{Term}$).
149−\item Retrieve the local context $\Gamma$ at the current sub goal
150−($\MO{Context}$).
147+\item Get the type of the current sub-goal ($\MO{Type}$)
148+\item Get the current proof term ($\MO{Term}$)
149+\item Retrieve the local context $\Gamma$ at the current sub-goal
150+($\MO{Context}$)
151151\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative
152−to $\Gamma$.
152+to $\Gamma$
153153\end{itemize}
154−\item \demph{Unification}, which unifies two terms (potentially solving sub
155−goals) relative to $\Gamma$. This may introduce new unification problems
156−to the proof state.
157−\item \demph{Tactics} which update the proof term. Tactics operate on the sub term
158−at the binder specified by the head of the hole queue $\vQ$.
159−\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the
160−head of the hole queue.
161−%\item \demph{Deferring} a sub goal, which adds a new definition to the global context
162−%$\vC$ which solves the sub goal.
154+\item \demph{Unification}, which unifies two terms (potentially solving sub-goals) relative to $\Gamma$. This may introduce new unification problems
155+to the proof state
156+\item \demph{Tactics} which update the proof term. Tactics operate on the sub-term
157+at the binder specified by the head of the hole queue $\vQ$
158+\item \demph{Focussing} on a specific sub-goal, which brings a different sub-goal to the
159+head of the hole queue
160+%\item \demph{Deferring} a sub-goal, which adds a new definition to the global context
161+%$\vC$ which solves the sub-goal.
163162\end{itemize}
164163
165164Elaboration of an \Idris{} expression involves creating a new proof state,
@@ -307,7 +306,7 @@ of $\vt$. Tactics may also have the side effect of updating the proof state,
307306therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
308307
309308Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
310−given in Figure \ref{runtac} which
309+given in Figure \ref{runtac}, which
311310locates the appropriate sub-term, applies the tactic with the context
312311local to this sub-term, and
313312replaces the sub-term with the term returned by the
@@ -386,12 +385,13 @@ Unification is crucial to the success of elaboration --- it is unification
386385which finds values of implicit arguments, in particular. We do not require
387386unification to succeed immediately, in general, as instantiating a hole may
388387affect the solution to other unification problems. Instead,
389−$\MO{PrimUnify}$ may give one of the following results:
388+$\PrimUnify\:\ve_1\:\ve_2$ may give one of the following results:
390389
391390\begin{itemize}
392391\item $\MO{Success}\;(\tx=\te, \tp)$, containing the solved holes mapping
393392$\vx$ to $\ve$, and a possibly empty set of blocked unification problems $\tp$.
394−If $\tp$ is empty, there is a solution for $\ve_1$ and $\ve_2$.
393+If $\tp$ is empty, there is a solution unifying $\ve_1$ and $\ve_2$ in
394+the context $\Gamma$.
395395\item $\MO{Failure}\;\ve$, if no solution is found due to a failure to unify
396396sub-terms in normal form.
397397\end{itemize}
@@ -543,8 +543,8 @@ problem) and is handled by $\MO{Try}$.
543543
544544\subsubsection{Creating binders}
545545
546−We also define primitive tactics for constructing binders. Creating a $\lambda$
547−binding requires that the goal normalises to a function type:
546+We also define primitive tactics for constructing binders. Creating a
547+$\lambda$-binding requires that the goal normalises to a function type:
548548
549549\DM{
550550\PA{\A\A}{
@@ -627,7 +627,7 @@ entirety of $\vx\;\ve$, and the resulting term is not well-typed:
627627
628628\noindent
629629If, on the other hand, we $\MO{Attack}$ the hole then instantiate it with
630−a $\lambda$ binding $\vn$, we get:
630+a $\lambda$-binding $\vn$, we get:
631631
632632\DM{
633633\begin{array}{ll}
@@ -668,7 +668,7 @@ building the right hand side.
668668
669669To illustrate how tactics are applied, using $\MO{Tactic}$, to build a
670670complete term by refining a proof state, let us consider the following
671−\TT{} definition for the identify function:
671+\TT{} definition for the identity function:
672672
673673\DM{
674674\AR{
@@ -866,7 +866,7 @@ a Coq proof script.
866866{Building $\FN{id}$ with tactics}
867867{idelab}
868868
869−%--- give unify in full, esp. as it solves sub goals? Maybe...
869+%--- give unify in full, esp. as it solves sub-goals? Maybe...
870870
871871% Unify' G x t = Success (x, t) if ?x : t in G
872872% Unify' G t x = Success (x, t) if ?x : t in G
@@ -1347,7 +1347,7 @@ to the global context, such as definitions in $\iwhere$ clauses.
13471347First, let us consider the simplest case, with no $\iwhere$ clause:
13481348
13491349\DM{
1350−\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;?
1350+\MO{ElabClause}\;(\vx\;\ttt\;=\;\ve)\;\mq\;\ldots
13511351}
13521352
13531353How does the left hand side get elaborated, given that elaboration is type directed, and
@@ -1396,9 +1396,10 @@ the clauses and adding the resulting collection to \TT{}.
13961396}
13971397
13981398Elaborating a clause is made only slightly more complex by the presence of
1399−$\iwhere$ clauses. In this case, after elaborating the left hand side, the pattern
1400−bound variables are added as extra arguments to the declarations in the $\iwhere$ block,
1401−which are then recursively elaborated before the right hand side.
1399+$\iwhere$ clauses. In this case, after elaborating the left hand side, the
1400+pattern-bound variables are added as extra arguments to the declarations in the
1401+$\iwhere$ block, which are then recursively elaborated before the right hand
1402+side.
14021403
14031404\DM{
14041405\AR{
@@ -1419,7 +1420,7 @@ which are then recursively elaborated before the right hand side.
14191420}
14201421
14211422In \TT{}, all definitions must be at the top level. Therefore, the declarations
1422−in the $\iwhere$ block are lifted out, adding the pattern bound names as additional arguments
1423+in the $\iwhere$ block are lifted out, adding the pattern-bound names as additional arguments
14231424to ensure they are in scope, using the $\MO{Lift}$ operation. This also modifies
14241425the right hand side $\ve$ to use the lifted definitions, rather than the original.
14251426
@@ -1438,7 +1439,7 @@ This is equivalent to the following, using top-level definitions only:
14381439\begin{SaveVerbatim}{natToBinw}
14391440
14401441natToBin : Nat -> List Bool
1441−natToBin O = Nil
1442+natToBin Z = Nil
14421443natToBin k = natToBin' k (parity k)
14431444
14441445\end{SaveVerbatim}
@@ -1582,7 +1583,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
15821583showNat : Show Nat
15831584showNat = InstanceShow show' where
15841585 show' : Nat -> String
1585− show' O = "O"
1586+ show' Z = "Z"
15861587 show' (S k) = "s" ++ show k
15871588
15881589\end{SaveVerbatim}