@@ -187,18 +187,58 @@ $\Eval\:\ve\:\mq\:\vv$ means that evaluating the expression $\ve$ returns the
187value $\vv$.
187value $\vv$.
188\item $\MO{Unify}$, which unifies two well-typed expressions.
188\item $\MO{Unify}$, which unifies two well-typed expressions.
190−$\Unify\:\ve_1\:\ve_2\:\mq\:\tv$ means that unifying $\ve_1$ and $\ve_2$ produces a
190+$\Unify\:\ve_1\:\ve_2\:\mq\:\tu$ means that unifying $\ve_1$ and $\ve_2$ produces a
191−mapping $\tv$ from hole names to the values the holes must be instantiated with for
191+mapping $\tu$ from hole names to the values the holes must be instantiated with for
192$\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
192$\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
193(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
193(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
194if it cannot find such a mapping.
194if it cannot find such a mapping.
195\end{itemize}
195\end{itemize}
197\remph{Tactics} are specifically meta-operations which operate on the sub-term given
197\remph{Tactics} are specifically meta-operations which operate on the sub-term given
198−by the hole at the head of the hole queue in the proof state.
198+by the hole at the head of the hole queue in the proof state. They take the following form:
202+\MO{Tactic}_\Gamma & \vec{\VV{args}} & \vt & \MoRet{\vt'}
206+A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed by the sub-term $\vt$
207+on which it is operating. It runs relative to a context $\Gamma$ which contains all the bindings
209+in scope at that point in the term. The sub-term $\vt$ will either be a hole binding
210+$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The tactic returns a
211+new term $\vt'$ which can take any form, provided it is well-typed. Tactics are executed by a higher
212+level meta-operation $\MO{RunTac}$, which locates the appropriate sub-term, replaces it with the
213+term returns by the tactic, updates the hole queue in the proof state, and updates holes which
214+have been solved by unification.
216+Creating and destroying holes: Claim, Fill, Solve
220+\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
221+ \MoRet{\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
201−Creating and destroying holes: Claim, Exact, Solve
225+\DM{
227+\MO{Fill}_\Gamma & \vv & (\hole{\vx}{\vT}\SC\ve) &
228+ \MoRet{\RW{do}\:\AR{
229+ (\vv',\vT') \leftarrow \Check\:\vv\\
231+ \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\SC\ve}
238+\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
239+ \MoRet{\ve[\vv/\vx]}
203Attack, Lambda, Pi, Let
243Attack, Lambda, Pi, Let