[Tried fixing the bug, but ended up just moving it around.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080207022519] hunk ./HuttonsRazor.agda 193
-      -- Also make sure that the semantics of continuations does not
-      -- refer to Step₁.eval (via Step₁.c₂).
-
hunk ./HuttonsRazor.agda 196
-      ⟦_⟧c' : Cont -> Step₁.Cont
-      ⟦ c ⟧c' n = witness (cSem c n)
-
hunk ./HuttonsRazor.agda 198
-      evalP (val n) c = ▷ begin
-        ⟦ c ⟧c n
-          ≡⟨ proof (cSem c n) ⟩
-        ⟦ c ⟧c' n
-          ∎
+      evalP (val n)   c = ▷ begin ⟦ c ⟧c n ∎
hunk ./HuttonsRazor.agda 207
+    mutual
+
+      -- Also make sure that the semantics of continuations does not
+      -- refer to Step₁.eval (via Step₁.c₂).
+
+      ⟦_⟧c' : Cont -> Step₁.Cont
+      ⟦ c ⟧c' n = witness (cSem c n)
+
+      eval' : Expr -> Cont -> ℕ
+      eval' e c = witness (evalP' e c)
+
hunk ./HuttonsRazor.agda 226
+          ≡⟨ proof (evalP' e (c₃ n c)) ⟩
+        eval' e (c₃ n c)
hunk ./HuttonsRazor.agda 235
+      -- Note that eval above uses ⟦_⟧c, so it has to be updated.
+
+      evalP' : (e : Expr) (c : Cont) ->
+               EqualTo (eval e c)
+      evalP' (val n) c = ▷ begin
+        ⟦ c ⟧c n
+          ≡⟨ proof (cSem c n) ⟩
+        ⟦ c ⟧c' n
+          ∎
+      evalP' (e₁ ⊕ e₂) c = ▷ begin
+        eval e₁ (c₂ e₂ c)
+          ≡⟨ proof (evalP' e₁ (c₂ e₂ c)) ⟩
+        eval' e₁ (c₂ e₂ c)
+          ∎
+
hunk ./HuttonsRazor.agda 253
-    ⟦ e ⟧' = eval e c₁
+    ⟦ e ⟧' = eval' e c₁
hunk ./HuttonsRazor.agda 261
+      eval e c₁
+        ≡⟨ proof (evalP' e c₁) ⟩
hunk ./HuttonsRazor.agda 276
-    -- I tried to fix their mistake (see the val case of Step₂.evalP),
-    -- but this makes the termination checker complain.
+    -- I tried to fix their mistake, but this makes the termination
+    -- checker complain.
hunk ./HuttonsRazor.agda 280
-      using (Cont; eval)
+      using (Cont; correct)
hunk ./HuttonsRazor.agda 282
-               ; ⟦_⟧c' to exec; ⟦_⟧' to run
+               ; eval' to eval; ⟦_⟧c' to exec; ⟦_⟧' to run