From b5e3e5a23b99927db06a927f4ec236cd431cf7d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com> Date: Fri, 1 Apr 2022 19:11:56 +0900 Subject: [PATCH] Minor edit of README.md --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 955f1b96..7dbf2b95 100644 --- a/README.md +++ b/README.md @@ -61,10 +61,11 @@ followed by `make build-dep`. ## Where to Find the Proof Rules From the Paper The derived rules mentioned in the paper can be found [here](theories/typing/examples/derived_rules.v). -### Type System Rules + +### Type System Rules --- from the RustBelt Paper The files in [typing](theories/typing) prove semantic versions of the proof -rules given in the (RustBelt) paper. Notice that mutable borrows are called +rules given in the *RustBelt* paper. Notice that mutable borrows are called "unique borrows" in the Coq development. | Proof Rule | File | Lemma | -- GitLab