@@ -266,8 +266,8 @@ removes a hole from the head of the queue:
266266
267267\DM{
268268\AR{
269−\MO{NewHole}\;=\;\RW{do}\;\AR{
270−(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
269+\MO{NewHole}\;\vn\;=\;\RW{do}\;\AR{
270+(\vC,\Delta,\ve,\vP,\vQ)\gets\MO{Get}\\
271271\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ)\\
272272}
273273\\
@@ -312,7 +312,8 @@ given in Figure \ref{runtac} which
312312locates the appropriate sub-term, applies the tactic with the context
313313local to this sub-term, and
314314replaces the sub-term with the term returned by the
315−tactic.
315+tactic. Note that monadic lifting is left implicit in this Figure, so that
316+the details of the algorithm are not obscured.
316317% It then updates the hole queue in the proof state, and updates holes which have
317318% been solved by unification. If the tactic creates new holes, these are automatically
318319% added to the \remph{head} of the hole queue.
@@ -322,7 +323,7 @@ tactic.
322323\MO{Tactic}\;\VV{tac}\;=\;\RW{do}\;\AR{
323324\ve\Gets\MO{Term}\\
324325\vh\Gets\MO{NextHole}\\
325−\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\;\VV{tac}\;\vh\\
326+\ve'\Gets\MO{Tactic'}\;\langle\rangle\;\ve\\
326327\MO{SetTerm}\;\ve'
327328}
328329\medskip
@@ -331,8 +332,23 @@ tactic.
331332\RW{where} \\
332333& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)
333334& \MoRet{\VV{tac}_\Gamma\;(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\
335+& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)
336+& \MoRet{
337+\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
338+\RW{return}\;(\hole{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\hole{\vx}{\vT'})\;\ve)
339+\hg\RW{otherwise}}
340+}
341+\\
334342& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)
335343& \MoRet{\VV{tac}_\Gamma\;(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\;\vx=\vh} \\
344+
345+& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)
346+& \MoRet{\RW{do}\;\AR{\vv'\Gets\;\MO{Tactic'}\;\Gamma\;\vv\\
347+\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
348+\RW{return}\;(\guess{\vx}{\vT'}{\vv'}\SC
349+\MO{Tactic'}\;(\Gamma;\guess{\vx}{\vT'}{\vv'}\;\ve)
350+\hg\RW{otherwise}}} \\
351+
336352& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
337353& \MoRet{
338354\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
@@ -345,11 +361,11 @@ tactic.
345361\RW{return}\;(\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve)}
346362}
347363\\
348−& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)
349−& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\
364+& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vv\Hab\vT\SC\ve)
365+& \MoRet{\RW{do}\;\AR{\vv'\Gets\;\MO{Tactic'}\;\Gamma\;\vv\\
350366\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
351−\RW{return}\;(\LET\;\vx\defq\vt'\Hab\vT'\SC
352−\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve)}} \\
367+\RW{return}\;(\LET\;\vx\defq\vv'\Hab\vT'\SC
368+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vv'\Hab\vT')\;\ve)}} \\
353369& \MO{Tactic'} & \Gamma & (\vf\;\va) &
354370\MoRet{\RW{return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\
355371& \MO{Tactic'} & \Gamma & \vt & \MoRet{\RW{return}\;\vt}
@@ -429,7 +445,8 @@ keeping $\vx$ at the head:
429445\PA{\A\A}{
430446\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
431447 \MoRet{\RW{do}\;\AR{\MO{NewHole}\;\vy\\
432− \RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve}} \\
448+ \MO{Focus}\:\vx\\
449+ \RW{return}\;\hole{\vy}{\vS}\SC\hole{\vx}{\vT}\SC\ve}} \\
433450}
434451}
435452
@@ -692,23 +709,21 @@ the goal type.
692709\medskip
693710\\
694711\mbox{Initial state}
695−& \hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx
712+& \underline{\hole{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vx}
696713& \langle\vx\rangle \\
697714%
698715\MO{Attack} &
699−\underline{
700716\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
701−\hole{\vh_0}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vh_0
717+\underline{\hole{\vh_0}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}\SC\vh_0}
702718}
703719\SC\vx
704−}
705720&
706721\langle\vh_0,\vx\rangle\\
707722%
708723\MO{Lambda}\;\vA &
709724\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
710−\underline{
711−\lam{\vA}{\Type}\SC\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
725+\lam{\vA}{\Type}\SC\underline{
726+\hole{\vh_0}{\all{\va}{\vA}\SC\vA}\SC\vh_0
712727}
713728}
714729\SC\vx
@@ -718,12 +733,12 @@ the goal type.
718733\MO{Attack} &
719734\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
720735\lam{\vA}{\Type}\SC
721−\underline{
722736\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
723−{\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}
737+{
738+\underline{
739+\hole{\vh_1}{\all{\va}{\vA}\SC\vA}\SC\vh_1}}
724740\SC\vh_0
725741}
726−}
727742\SC\vx
728743&
729744\langle\vh_1,\vh_0,\vx\rangle\\
@@ -733,8 +748,8 @@ the goal type.
733748\lam{\vA}{\Type}\SC
734749\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
735750{
736−\underline{
737−\lam{\va}{\vA}\SC\hole{\vh_1}{\vA}\SC\vh_1
751+\lam{\va}{\vA}\SC\underline{
752+\hole{\vh_1}{\vA}\SC\vh_1
738753}
739754}
740755\SC\vh_0
@@ -746,9 +761,10 @@ the goal type.
746761\MO{Fill}\;\va &
747762\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
748763\lam{\vA}{\Type}\SC
749−\\
750−&
751−\hg\hg\hg\hg\hg\hg\hg\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
764+%\\
765+%&
766+%\hg\hg\hg\hg\hg\hg\hg
767+\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
752768{
753769\lam{\va}{\vA}\SC
754770\underline{
@@ -764,37 +780,35 @@ the goal type.
764780\MO{Solve} &
765781\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
766782\lam{\vA}{\Type}\SC
783+\underline{
767784\guess{\vh_0}{\all{\va}{\vA}\SC\vA}
768785{
769786\lam{\va}{\vA}\SC
770−\underline{
771787\va
772788}
773−}
774789\SC\vh_0
775790}
791+}
776792\SC\vx
777793&
778794\langle\vh_0,\vx\rangle\\
779795%
780796\MO{Solve} &
797+\underline{
781798\guess{\vx}{\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA}{
782799\lam{\vA}{\Type}\SC
783−\underline{
784800\lam{\va}{\vA}\SC
785801\va
786802}
787−}
788803\SC\vx
804+}
789805&
790806\langle\vx\rangle\\
791807%
792808\MO{Solve} &
793−\underline{
794809\lam{\vA}{\Type}\SC
795810\lam{\va}{\vA}\SC
796811\va
797−}
798812&
799813\langle\rangle\\
800814