[Rearranged the code.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101117135042
 Ignore-this: 62881472d7af291f4780937271e99452
] hunk ./CompositionBased.agda 14
+import Derivation
hunk ./CompositionBased.agda 162
-  open import Derivation
-  open P.≡-Reasoning
-  open Defunctionalised using (Term; return⊙; sub⊙; halt)
+  open Derivation
+  open Compositional using (⟦_⟧↑)
+  open Defunctionalised using (Term; return⊙; sub⊙; halt; comp)
hunk ./CompositionBased.agda 179
+      where open P.≡-Reasoning
hunk ./CompositionBased.agda 183
+      where open P.≡-Reasoning
hunk ./CompositionBased.agda 185
+      where open P.≡-Reasoning
+
+  correct : ∀ e → ⟦ e ⟧ ≡ exec (comp e halt) []
+  correct e = H.≅-to-≡ (begin
+    ! ⟦ e ⟧↑                                      ≡⟨ P.refl ⟩
+    ⟦ e ⟧                                         ≅⟨ !-cong (Defunctionalised.correct e) ⟩
+    ! (Defunctionalised.exec (comp e halt))       ≡⟨ P.refl ⟩
+    app (Defunctionalised.exec (comp e halt)) []  ≡⟨ proj₂ $ exec′ (comp e halt) [] ⟩
+    exec (comp e halt) []                         ∎)
+    where open H.≅-Reasoning
hunk ./CompositionBased.agda 201
-  open H.≅-Reasoning
-
hunk ./CompositionBased.agda 211
-  correct e = H.≅-to-≡ (begin
-    ⟦ e ⟧                                    ≅⟨ !-cong (Defunctionalised.correct e) ⟩
-    ! (Defunctionalised.exec (comp e))       ≡⟨ P.refl ⟩
-    app (Defunctionalised.exec (comp e)) []  ≡⟨ proj₂ $ Stack.exec′ (comp e) [] ⟩
-    exec (comp e)                            ∎)
+  correct = Stack.correct