Skip to content

Commit ba09176

Browse files
ibbemibbem
committed
Reformat the paper <-> artifact correspondence table
This is a purely source code cosmetic change. The markdown rendering isn't influenced at all by this change.
1 parent 2fe184e commit ba09176

1 file changed

Lines changed: 5 additions & 5 deletions

File tree

‎README.md‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -287,8 +287,8 @@ For details about Agda's library management, please have a look at [Agda's packa
287287
Our Agda formalization exhaustively formalizes all definitions, theorems, and proofs from our paper.
288288
The following table shows where each of the definitions, theorems, and proofs from the paper are formalized in this library.
289289

290-
| statement | notation in paper | name in our Agda Library | file | notes |
291-
|-----------------|-----------------------------------|--------------------------------------------------------------------|------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------|
290+
| statement | notation in paper | name in our Agda Library | file | notes |
291+
|-----------------|-----------------------------------|--------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------|
292292
| Section 1 | contribution: a map of languages | | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | |
293293
| Section 2 | running example | | [src/Vatras/Test/Experiments/RoundTrip.agda](src/Vatras/Test/Experiments/RoundTrip.agda) | |
294294
| Table 1 | | | [src/Vatras/Lang/All.agda](src/Vatras/Lang/All.agda) | This file only reexports the language definitions. Use the go-to-definition functionality of your editor for easy exploration. |
@@ -305,9 +305,9 @@ The following table shows where each of the definitions, theorems, and proofs fr
305305
| | Equivalence ≅ | `_≅_`, `_≅[_][_]`_ | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The difference between `_≅_` and `_≅[_][_]_` is the same as between `_⊆_` and `_⊆[_]_`. |
306306
| Corollary 4.5 | ⊑ is a partial order | `⊆-IsIndexedPartialOrder`, `⊆[]-refl`, `⊆[]-antisym`, `⊆[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | |
307307
| | ≅ is an equivalence relation | `≅-IsIndexedEquivalence`, `≅[]-refl`, `≅[]-sym`, `≅[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | |
308-
| Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. |
308+
| Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. |
309309
| Definition 4.8 | Non-empty Indexed Set | `empty` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The library definition is a predicate that ensures an indexed set to be non-empty. |
310-
| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. |
310+
| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. |
311311
| Definition 4.10 | Semantic Domain | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | In contrast to a variant generator, the semantic domain is the type of variant generators instead of its elements. |
312312
| Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | |
313313
| Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | |
@@ -320,7 +320,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
320320
| | ≻ | `_≻_` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
321321
| Corollary 4.18 | ⪰ is a partial order | `≽-IsPartialOrder` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
322322
| | ≡ is an equivalence relation | `≋-IsEquivalence` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
323-
| Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. |
323+
| Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. |
324324
| Definition 4.20 | 𝑀 ⇾ 𝐿 correct | `LanguageCompiler` | [src/Vatras/Framework/Compiler.agda](src/Vatras/Framework/Compiler.agda) | |
325325
| Theorem 4.21 | 𝑀 ⇾ 𝐿 ⇒ 𝐿 ⪰ 𝑀 | `expressiveness-from-compiler` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
326326
| Theorem 4.22 | Complete(M) ∧ L ≽ M ⇒ Complete(L) | `completeness-by-expressiveness` | [src/Vatras/Framework/Proof/ForFree.lagda.md](src/Vatras/Framework/Proof/ForFree.lagda.md) | |

0 commit comments

Comments
 (0)