@@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
5959---- The Effect EDSL itself ----
6060
6161-- some proof automation
62−findEffElem : Nat -> Tactic -- Nat is maximum search depth
63−findEffElem O = Refine "Here" `Seq` Solve
64−findEffElem (S n) = GoalType "EffElem"
62+findEffElem : Nat -> List (TTName, Binder TT) -> Tactic -- Nat is maximum search depth
63+findEffElem O ctxt = Refine "Here" `Seq` Solve
64+findEffElem (S n) ctxt = GoalType "EffElem"
6565 (Try (Refine "Here" `Seq` Solve)
66− (Refine "There" `Seq` (Solve `Seq` findEffElem n)))
66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt)))
6767
68−findSubList : Nat -> Tactic
69−findSubList O = Refine "SubNil" `Seq` Solve
70−findSubList (S n)
68+findSubList : Nat -> List (TTName, Binder TT) -> Tactic
69+findSubList O ctxt = Refine "SubNil" `Seq` Solve
70+findSubList (S n) ctxt
7171 = GoalType "SubList"
7272 (Try (Refine "subListId" `Seq` Solve)
7373 ((Try (Refine "Keep" `Seq` Solve)
74− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt))
7575
7676updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
7777 List EFFECT
@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->
116116-- Eff : List (EFFECT m) -> Type -> Type
117117
118118implicit
119−lift' : {default tactics { reflect findSubList 100; solve; }
119+lift' : {default tactics { applyTactic findSubList 100; solve; }
120120 prf : SubList ys xs} ->
121121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
122122lift' {prf} e = lift prf e
123123
124124implicit
125125effect' : {a, b: _} -> {e : Effect} ->
126− {default tactics { reflect findEffElem 100; solve; }
126+ {default tactics { applyTactic findEffElem 100; solve; }
127127 prf : EffElem e a xs} ->
128128 (eff : e a b t) ->
129129 EffM m xs (updateResTy xs prf eff) t