From: Ralf Jung <post@ralfj.de>
Date: Fri, 6 Apr 2018 11:09:55 +0000 (+0200)
Subject: no multi-defn boxes
X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/126a0604a09fd8f572f688e56a1abe58278d76a6?ds=sidebyside;hp=ee3b920271648a553bf01a673a25d305d95b36d3

no multi-defn boxes
---

diff --git a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
index 4aed608..98e0477 100644
--- a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -154,6 +154,8 @@ Formally:
 ```
 Box<T>.own(bytes) := exists |ptr, inner_bytes| bytes.try_into() == Ok(ptr) &&
   ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```
 (&'a mut T).own(bytes) := exists |ptr| bytes.try_into() == Ok(ptr) &&
   borrowed('a,
     exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
@@ -166,6 +168,8 @@ This could look as follows:
 ```
 Box<T>.own(ptr: Pointer) :=
   exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes)
+```
+```
 (&'a mut T).own(ptr: Pointer) :=
   borrowed('a, exists |inner_bytes| ptr.points_to_owned(inner_bytes) && T.own(inner_bytes))
 ```
@@ -223,6 +227,8 @@ A list of bytes makes a valid `PinBox<T>` if those bytes form a pointer `ptr` su
 For `Pin<'a, T>`, `ptr` is valid if we have borrowed `T.pin(ptr)` for lifetime `'a`.
 ```
 PinBox<T>.own(ptr) := T.pin(ptr)
+```
+```
 Pin<'a, T>.own(ptr) := borrowed('a, T.pin(ptr))
 ```