[Removed an unnecessary part of the compiler correctness statement.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080616170052] move ./CompilerCorrectness/Completeness1.agda ./CompilerCorrectness/Completeness.agda
move ./CompilerCorrectness/Completeness2.agda ./CompilerCorrectness/BarTheorem.agda
hunk ./CompilerCorrectness.agda 58
--- The third part of completeness: If the program must terminate,
--- then some final state _will_ be reached.
-
--- Note that this result actually implies Sound₁, if restricted to
--- total input (see Bar.bar-lemma).
-
-Complete₃ : forall {t} -> Expr t -> Status -> Set
-Complete₃ e i = ¬ e ⇑[ i ] -> start e i ◁ Matches e i
-
hunk ./CompilerCorrectness.agda 61
-Complete e i = Complete₁ e i × Complete₂ e i × Complete₃ e i
+Complete e i = Complete₁ e i × Complete₂ e i
hunk ./CompilerCorrectness/BarTheorem.agda 5
-module CompilerCorrectness.Completeness2 where
+-- This theorem is currently unused.
+
+module CompilerCorrectness.BarTheorem where
hunk ./CompilerCorrectness/BarTheorem.agda 261
--- The third part of the completeness proof.
-
-complete₃ : forall {t} (e : Expr t) {i} -> Complete₃ e i
-complete₃ e ¬⇑ = ◁-map Matches⁺⇒Matches (bar-theorem e ¬⇑)
-
hunk ./CompilerCorrectness/Completeness.agda 5
-module CompilerCorrectness.Completeness1 where
+module CompilerCorrectness.Completeness where
hunk ./CompilerCorrectness/Proof.agda 9
-open import CompilerCorrectness.Completeness1
-open import CompilerCorrectness.Completeness2
+open import CompilerCorrectness.Completeness
hunk ./CompilerCorrectness/Proof.agda 15
-correct e = (sound e , (\{_} -> complete₁ e) , complete₂ , complete₃ e)
+correct e = (sound e , (\{_} -> complete₁ e) , complete₂)
hunk ./Everything.agda 59
-import CompilerCorrectness.Completeness1
-import CompilerCorrectness.Completeness2
+import CompilerCorrectness.Completeness
+import CompilerCorrectness.BarTheorem  -- Currently unused.