@@ -146,27 +146,14 @@ effect' : {a, b: _} -> {e : Effect} ->
146146 EffM m xs (updateResTy xs prf eff) t
147147effect' {prf} e = effect prf e
148148
149−data WrapEffM : (m : Type -> Type) ->
150− List EFFECT -> List EFFECT -> Type -> Type where
151− WEffM : EffM m xs xs' t -> WrapEffM m xs xs' t
152−
153−-- wrap subprograms to prevent lifting (need to guarantee same effects as
154−-- parent!)
155−
156−test_lbl' : {x : lbl} ->
157− {default tactics { applyTactic findEffElem 20; solve; }
158− prf : EffElem e (LRes x (Either l r)) xs} ->
159− WrapEffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
160− WrapEffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
161− EffM m xs xs' t
162−test_lbl' {prf} (WEffM l) (WEffM r) = test_lbl prf l r
163−
164−test' : {default tactics { applyTactic findEffElem 20; solve; }
165− prf : EffElem e (Either l r) xs} ->
166− EffM m (updateResTyImm xs prf l) xs' t ->
167− EffM m (updateResTyImm xs prf r) xs' t ->
168− EffM m xs xs' t
169−test' {prf} l r = test prf l r
149+-- For making proofs implicitly for 'test' and 'test_lbl'
150+
151+syntax if_valid then [e] else [t] =
152+ test (tactics { applyTactic findEffElem 20; solve; }) t e
153+
154+syntax if_valid [lbl] then [e] else [t] =
155+ test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e
156+
170157
171158-- for 'do' notation
172159