From 776a7621874db9a38c27a5801817b17c11760a6a Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 2 Jul 2024 12:25:54 +0200 Subject: [PATCH] README: repair false links in table --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 254596d0..16b2b09c 100644 --- a/README.md +++ b/README.md @@ -292,7 +292,7 @@ The following table shows where each of the definitions, theorems, and proofs fr | | Equivalence ≅ | `_≅_`, `_≅[_][_]`_ | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | The difference between `_≅_` and `_≅[_][_]_` is the same as between `_⊆_` and `_⊆[_]_`. | | Corollary 4.5 | ⊑ is a partial order | `⊆-IsIndexedPartialOrder`, `⊆[]-refl`, `⊆[]-antisym`, `⊆[]-trans` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | | | ≅ is an equivalence relation | `≅-IsIndexedEquivalence`, `≅[]-refl`, `≅[]-sym`, `≅[]-trans` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | -| Definition 4.6 | Finite Indexed Set | | [ | We]( | We) actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. | +| Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. | | Definition 4.8 | Non-empty Indexed Set | `empty` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | The library definition is a predicate that ensures an indexed set to be non-empty. | | Definition 4.9 | Variant Map | `VMap` | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda) | This is the finite and non-empty indexed set definition mentioned above. | | Definition 4.10 | Semantic Domain | `VMap` | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. | @@ -307,7 +307,7 @@ The following table shows where each of the definitions, theorems, and proofs fr | | ≻ | `_≻_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | | Corollary 4.18 | ⪰ is a partial order | `≽-IsPartialOrder` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | | | ≡ is an equivalence relation | `≋-IsEquivalence` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| Definition 4.19 | 𝑀 ⇾ 𝐿 | | [ | We]( | We) only model correct compilers. | +| Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. | | Definition 4.20 | 𝑀 ⇾ 𝐿 correct | `LanguageCompiler` | [src/Framework/Compiler.agda](src/Framework/Compiler.agda) | | | Theorem 4.21 | 𝑀 ⇾ 𝐿 ⇒ 𝐿 ⪰ 𝑀 | `expressiveness-from-compiler` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | | Theorem 4.22 | Complete(M) ∧ L ≽ M ⇒ Complete(L) | `completeness-by-expressiveness` | [src/Framework/Proof/Transitive.lagda.md](src/Framework/Proof/Transitive.lagda.md) | |