@@ -257,14 +257,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
257 return $ VBind True -- (vinstances 0 sc < 2)
257 return $ VBind True -- (vinstances 0 sc < 2)
258 n' b' (\x -> ev ntimes stk False ((n, x):env) sc)
258 n' b' (\x -> ev ntimes stk False ((n, x):env) sc)
259 where vbind env t
259 where vbind env t
261−-- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
262−-- stk top env (finalise tm)) t
264 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
260 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
261+ -- Treat "assert_total" specially, as long as it's defined!
265− ev ntimes stk top env (App (App (P _ (UN at) _) _) arg)
262+ ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
263+ | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,
266− | at == txt "assert_total" && not simpl
264+ at == txt "assert_total" && not simpl
267− = ev ntimes (UN at : stk) top env arg
265+ = ev ntimes (n : stk) top env arg
268 ev ntimes stk top env (App f a)
266 ev ntimes stk top env (App f a)
269 = do f' <- ev ntimes stk False env f
267 = do f' <- ev ntimes stk False env f
270 a' <- ev ntimes stk False env a
268 a' <- ev ntimes stk False env a