Skip to content

Commit

Permalink
README: repair false links in table
Browse files Browse the repository at this point in the history
  • Loading branch information
@pmbittner
pmbittner committed Jul 2, 2024
1 parent 9ea29ea commit 776a762
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. |
Expand All @@ -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) | |
Expand Down

0 comments on commit 776a762

Please sign in to comment.