README: Remove TODOs not relevant for the artifact submission

VariantSync · Jul 3, 2024 · a8b86e7 · a8b86e7
1 parent df4ff68
commit a8b86e7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -372,7 +372,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
 | Figure 3        |                                   |                                                                    | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md)                         | This file mostly reexports expressiveness results and applies transitivity and the above theorems. It serves as a nice entry point to explore most of our results. |
 | Theorem 5.1     | 𝑛-CC                              | `NCC`                                                              | [src/Lang/NCC.lagda.md](src/Lang/NCC.lagda.md)                                                       |                                                                                                                                                                    |
 |                 | 𝑛-CC ⪰ CCC                        | `NCC≽CCC`                                                          | [src/Translation/Lang/CCC-to-NCC.agda](src/Translation/Lang/CCC-to-NCC.agda)                         |                                                                                                                                                                    |
-|                 | clamp                             | `Exact.translate`                                                  | [src/Translation/Lang/CCC-to-NCC.agda](src/Translation/Lang/CCC-to-NCC.agda)                         |                                                                                                                                                                    | -- TODO this is not actually a compiler
+|                 | clamp                             | `Exact.translate`                                                  | [src/Translation/Lang/CCC-to-NCC.agda](src/Translation/Lang/CCC-to-NCC.agda)                         |                                                                                                                                                                    |
 |                 | shrink₂                           | `shrinkTo2Compiler`                                                | [src/Translation/Lang/NCC/ShrinkTo2.agda](src/Translation/Lang/NCC/ShrinkTo2.agda)                   |                                                                                                                                                                    |
 |                 | grow                              | `growCompiler`                                                     | [src/Translation/Lang/NCC/Grow.agda](src/Translation/Lang/NCC/Grow.agda)                             |                                                                                                                                                                    |
 | Theorem 5.3     | ADT ≽ 2CC                         | `ADT≽2CC`                                                          | [src/Translation/Lang/2CC-to-ADT.agda](src/Translation/Lang/2CC-to-ADT.agda)                         |                                                                                                                                                                    |
@@ -392,7 +392,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
 | Theorem 5.16    | ¬Complete(FST)                    | `FST-is-incomplete`                                                | [src/Lang/FST.agda](src/Lang/FST.agda)                                                               |                                                                                                                                                                    |
 | Theorem 5.17    | OC ⋡ FST                          | `WFOC⋡FST`                                                         | [src/Translation/Lang/FST-to-OC.lagda.md](src/Translation/Lang/FST-to-OC.lagda.md)                   |                                                                                                                                                                    |
 | Theorem 5.18    | FST ⋡ OC                          | `FSTL⋡WFOCL`                                                       | [src/Translation/Lang/OC-to-FST.agda](src/Translation/Lang/OC-to-FST.agda)                           |                                                                                                                                                                    |
-| Corollary 5.19  | FST ⋡ 2CC                         | `FST⋡2CC`                                                          | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md)                         |                                                                                                                                                                    | -- TODO Why are both F's the same
+| Corollary 5.19  | FST ⋡ 2CC                         | `FST⋡2CC`                                                          | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md)                         |                                                                                                                                                                    |
 | Theorem 5.20    | Sound(FST)                        | `FST-is-sound`                                                     | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md)                         |                                                                                                                                                                    |
 |                 | 2CC ≽ FST                         | `2CC≽FST`                                                          | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md)                         |                                                                                                                                                                    |