From e9a9e56e268400d2f649f8c34fa7fb79371eca00 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 31 Oct 2018 20:56:47 +0100 Subject: [PATCH] README tweaks. --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index d129179..a389b96 100644 --- a/README.md +++ b/README.md @@ -30,9 +30,9 @@ Iron has been built and tested with the following dependencies specific to this logic that are used later. - The machinery for connecting the generalized proofmode/MoSeL from to - fractional predicates is contained in (theories/proofmode)[theories/proofmode]. + fractional predicates is contained in [theories/proofmode](theories/proofmode). -- In (theories/iron_logic)[theories/iron_logic] much of the core Iron logic +- In [theories/iron_logic](theories/iron_logic) much of the core Iron logic discussed in Section 2 is defined. * _Uniformity_ with respect to fractions is defined in [theories/iron_logic/iron.v](theories/iron_logic/iron.v) as `Uniform` and @@ -48,7 +48,7 @@ Iron has been built and tested with the following dependencies [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heapG`. So too are the definitions of ↦ and 𝖊 (in the formalization called `perm`). * The theorems stated in Section 5 about updates to the heap ghost - state are proven in (theories/heap_lang/heap.v)[theories/heap_lang/heap.v]. + state are proven in [theories/heap_lang/heap.v](theories/heap_lang/heap.v). * The state interpretation from Section 5 is defined in [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heap_ctx`. * Theorems 2.1, 2.2, 4.1, and 4.2 are proven in -- GitLab